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
