[klee-dev] klee memory access model and test cases

[Hank Zhang]

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
-------------- next part --------------
HTML attachment scrubbed and removed