From 4edbab2612e75aeb1f4f8f840c25993ff437c78c Mon Sep 17 00:00:00 2001 From: rubenasplund <ruben.asplund@hotmail.com> Date: Wed, 9 Dec 2020 13:53:45 +0100 Subject: [PATCH] Exercise A,B,C --- examples/get_sign.c | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/examples/get_sign.c b/examples/get_sign.c index 2cf5959..cc2dfd6 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 // -- GitLab