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

[Richard Rutledge]

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 <westrainzxh at gmail.com> 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
-------------- next part --------------
HTML attachment scrubbed and removed