diff --git a/examples/get_sign.c b/examples/get_sign.c index 2cf595996551871852cc969b39850317b6f5173c..0bf1df59594de2feafc6152fbe3540e090f3ea01 100644 --- a/examples/get_sign.c +++ b/examples/get_sign.c @@ -31,12 +31,23 @@ int main() // > klee get_sign.bc // // [your answer here] +/* +KLEE: output directory is "/home/ironedde/Documents/courses/D7020E/gits/klee_tutorial/klee-out-1" +KLEE: Using Z3 solver backend + +KLEE: done: total instructions = 31 +KLEE: done: completed paths = 3 +KLEE: done: generated tests = 3 +*/ // // B) Inspecting the output // // > ls klee-last/ // // [your answer here] +/* +lrwxrwxrwx 1 ironedde ironedde 69 Dec 12 14:41 klee-last -> /home/ironedde/Documents/courses/D7020E/gits/klee_tutorial/klee-out-1 +*/ // // C) Inspecting the generated test cases // @@ -45,17 +56,26 @@ int main() // What path in the code does this test represent? // // [your answer here] +/* +The path where x == 0. +*/ // // > ktest-tool klee-last/test000002.ktest // // What path in the code does this test represent? // // [your answer here] +/* +The path where x is a positive number. +*/ // > ktest-tool klee-last/test000003.ktest // // What path in the code does this test represent? // // [your answer here] +/* +The path where x is a negative number. +*/ // // D) Replaying a test case // @@ -109,6 +129,9 @@ int main() // Did the result correspond to the expected path for the test? // // [your answer here] +/* +Yes, the return status was 0. +*/ // // > KTEST_FILE=klee-last/test000002.ktest ./a.out // @@ -117,6 +140,9 @@ int main() // Did the result correspond to the expected path for the test? // // [your answer here] +/* +Yes, the return code has 1 corresponding to the possitve number. +*/ // // > KTEST_FILE=klee-last/test000003.ktest ./a.out // @@ -125,10 +151,16 @@ int main() // Did the result correspond to the expected path for the test? // // [your answer here] +/* +No, the returncode was 255 not -1 +*/ // // Why not? Confer to shell error codes: // // [your answer here] +/* +The return codes in bash is only between 0-255. Negative numbers gets mapped to 256 - [The negative number], in our case 256 - 1 = 255 which was our returncode. +*/ // // D) Debugging // @@ -153,6 +185,10 @@ int main() // What value do you get, and why? // // [your answer here] +/* +$1 = 0 +We got a zero because we ran the klee test where the input value was zero. +*/ // // Step the code // > (gdb) next @@ -160,6 +196,9 @@ int main() // What path did it take, and why? // // [your answer here] +/* +It took the path where x == 0 because this was the test where the input values was zero. +*/ // // Now we can try with another test: // @@ -173,6 +212,9 @@ int main() // Which path did it take, and why? // // [your answer here] +/* +It took the path where x was a positive number, because this was the test where the input values was 255. +*/ // // And finally: // @@ -181,6 +223,9 @@ int main() // Which path did it take, and why? // // [your answer here] +/* +It took the path where x was a negative number, because this was the test where the input values was negative. +*/ // // E) Under the hood. // @@ -190,6 +235,11 @@ int main() // // [your answer here] // (hint, mark memory region as symbolic) +/* +I had a hard time finding good resources for this information. +But my best guess is that, as the hint says, klee makes the memory region defined from the &a pointer and the size of the region as symbolic. +This in turn will allow klee to try any bitcode that fits in this memory region. +*/ // // Explain in your own words how // `klee_make_symbolic(&a, sizeof(a), "a");` @@ -198,3 +248,6 @@ int main() // [your answer here] // (hint, KTEST_FILE points to a concrete assignment // of the memory region) +/* +When you replay the testcases klee will replace the functioncall with an assignment of the variable a, corresonding to the testcase. +*/