diff --git a/examples/get_sign.c b/examples/get_sign.c index 2cf595996551871852cc969b39850317b6f5173c..cc2dfd656edd23dbfbf0cd3dead9414add6aa891 100644 --- a/examples/get_sign.c +++ b/examples/get_sign.c @@ -31,12 +31,16 @@ int main() // > klee get_sign.bc // // [your answer here] +// 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] +// assembly.ll info messages.txt run.istats run.stats test000001.ktest test000002.ktest test000003.ktest warnings.txt // // C) Inspecting the generated test cases // @@ -44,18 +48,19 @@ int main() // // What path in the code does this test represent? // -// [your answer here] +// [The first: return 0] // // > ktest-tool klee-last/test000002.ktest // // What path in the code does this test represent? // -// [your answer here] +// [The third: return 1] +// // > ktest-tool klee-last/test000003.ktest // // What path in the code does this test represent? // -// [your answer here] +// [The second: return -1] // // D) Replaying a test case //