You get multiple test cases even though there are no program branches due to the unconstrained buf indexed access.
To remain sound, klee forks a case for each value of index that could resolve to a memory object. The value corresponding to zero is the buf array. The other values resolve the access to other memory objects found in the virtual state. │⚙ Cheers! │Richard Rutledge └──────────────────── On Tue, Dec 4, 2018 at 9:52 PM, Hank Zhang <[email protected]> wrote: Hi all, I am new to klee, and I wrote a test case, but I do not understand the generated testcases, and the memory model of klee. I tried to search the email archive and other websites but no result. Here is my question. My simple program, test_main.c, looks like below: ``` #include <stdio.h> #include <klee/klee.h> int main(){ int i; klee_make_symbolic(&i, sizeof i, "sym_i"); char buf[20]; buf[i]=9; return 0; } ``` And then ``` clang -I /PATH/klee/include -emit-llvm -c test_main.c -o test_main.bc klee test_main.bc ``` After that, the result is: ``` KLEE: done: total instructions = 14 KLEE: done: completed paths = 5 KLEE: done: generated tests = 5 ``` Which means klee finds 5 paths and generate 5 tests. With this scripts I can see that the test cases are: $ for testfile in `ls klee-last/*.ktest`; do ktest-tool --write-ints $testfile |grep data; done ``` object 0: data: 536870912 object 0: data: -1216296 object 0: data: -1216208 object 0: data: 0 object 0: data: -1216288 ``` My question is, why klee finds 5 paths? and what are the meaning of generated 5 tests, especially the 3 negative ones? Thank you very much
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
