[klee-dev] KLEE make pointer symbolically

[张若虚]

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?


Thanks a lot!


Yifei
-------------- next part --------------
HTML attachment scrubbed and removed