diff --git a/examples/get_sign.c b/examples/get_sign.c index cc2dfd656edd23dbfbf0cd3dead9414add6aa891..6070b422af326a2592d3409b94bfec2b24281fb1 100644 --- a/examples/get_sign.c +++ b/examples/get_sign.c @@ -113,7 +113,7 @@ int main() // // Did the result correspond to the expected path for the test? // -// [your answer here] +// [YES] // // > KTEST_FILE=klee-last/test000002.ktest ./a.out // @@ -121,7 +121,7 @@ int main() // // Did the result correspond to the expected path for the test? // -// [your answer here] +// [YES] // // > KTEST_FILE=klee-last/test000003.ktest ./a.out // @@ -129,7 +129,7 @@ int main() // // Did the result correspond to the expected path for the test? // -// [your answer here] +// [NO] // // Why not? Confer to shell error codes: // @@ -157,14 +157,14 @@ int main() // // What value do you get, and why? // -// [your answer here] +// [$1 = 0] // // Step the code // > (gdb) next // // What path did it take, and why? // -// [your answer here] +// [Path return 0; becasue x == 0] // // Now we can try with another test: // @@ -177,7 +177,7 @@ int main() // // Which path did it take, and why? // -// [your answer here] +// [Path return 1; becasue x > 0] // // And finally: // @@ -185,7 +185,7 @@ int main() // // Which path did it take, and why? // -// [your answer here] +// [Path return -1; because x < 0] // // E) Under the hood. //