On 3 June 2015 at 05:28, 张若虚 <[email protected]> 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"); ``` _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
