Review

Examples:

Get_sign.rs:

B:

You should get three test cases, one for each of the generated paths.

C:

This could be due to a difference in versions, but my replayed test cases came back as:

test case 1: 1

test case 2: 0

test case 3: -1

Get_sign.c

B:

You should see an output similar to:

assembly.ll messages.txt run.stats test000002.ktest warnings.txt

info run.istats test000001.ktest test000003.ktest

C:

This could be due to a difference in versions again, I get the tesults:

test case 1: 0

test case 2: 1

test case 3: -1

D:

Here I’ve the results corresponding to the ones I’ve shown in C, I believe we’ve just gotten a different order on our tests.

E:

You’ve an entire question missing:

One is when the test cases are generated and the other when they are replayed.

Cargo_klee_examples:

get_sign.rs:

C:

It’s correct that it’s looking for the last modified .ll file, but where?

cyccnt.rs:

Looks good, nothing to change!

array.rs:

A:

Correct about the test cases, but why doesn’t the compiler optimize out b completely as it is an unused variable?