diff --git a/examples/get_sign.rs b/examples/get_sign.rs index 7028183536f6c3441fe9b4d626c587a0b11753ca..a7862fb79499a3cb1914bb16541890429f9466da 100644 --- a/examples/get_sign.rs +++ b/examples/get_sign.rs @@ -109,13 +109,17 @@ mod ll { // What was the generated hash. // // [your answer here] +// 85c57be6132dac1d // // B) Inspecting the test cases. // // Figure out to run `ktest-tool` on the generated test cases. // (Hint, it is just a matter of paths.) // -// [your answer here] +// [your answer here] TODO: What is the question here? +// ktest-tool target/debug/examples/klee-out-0/test000001.ktest x < 0 return -1 +// ktest-tool target/debug/examples/klee-out-0/test000002.ktest x > 0 retunr 1 +// ktest-tool target/debug/examples/klee-out-0/test000003.ktest x = 0 retunr 0 // // C) Replaying your test cases. // @@ -136,6 +140,7 @@ mod ll { // > ls *.o // // [your answer here] +// get_sign-85c57be6132dac1d.o // // Now we need to link it with the `libkleeRuntest`. // @@ -154,14 +159,17 @@ mod ll { // Now run the code in the debugger. What path was triggered. // // [your answer here] +// x < 0, return -1 // // Change to test000002, what path does it trigger. // // [your answer here] +// x > 0, return 1 // // And finally change to test000003, what path was triggered. // // [your answer here] +// x = 0, return 0 // // D) Remarks and conclusions. //