get_sign.c, All tasks done.

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. 
+*/