[klee-dev] KLEE make pointer symbolically

[Dan Liew]

On 3 June 2015 at 05:28, 张若虚 <zhangruoxu0830 at qq.com> wrote:
>
> Hi all,
>
> In the following program, I make a pointer symbolically.  The name of
> program file is array.c
>
> int main(int argc, char **argv) {
> int a = 0;
> int *p = &a;
> klee_make_symbolic(&p, sizeof(p), "a");
> *p = 1;
> return EXIT_SUCCESS;
> }
>
> I use the following command to invoke KLEE.
>
> klee --search=random-path array.o
>
> And KLEE finds 89 paths and generate 84 test cases.
>
> Firstly, did I make some mistake, like the parameter of function
> klee_make_symbolic() ? Or did I miss some KLEE command line options which
> can solve this problem?
>
> If I am correct, I don't think this is reasonable. Why does KLEE handle
> symbolic pointer in this way?

It's not exactly clear what your intention is but what KLEE is doing
perfectly reasonable. You made the pointer ``p`` symbolic so it can
point to anything (including ``a``) so KLEE's current approach is to
create a path for every possible memory object that could be pointed
to by the symbolic (I suspect KLEE also generates a path for the case
where the pointer does not point inside any memory object).

I noticed you set the third argument to ``klee_make_symbolic()`` to
"a" despite the fact the pointer ``p`` might not point to ``a``.
If you actually wanted to make the variable ``a`` symbolic you should do

```
klee_make_symbolic(&a, sizeof(a), "a");
```