[klee-dev] Query: Klee behavior with pointer de-referencing

[Sandeep]

Hello All,

Please consider the following program.

The intension of the program is to let KLEE choose a value of x  so that 
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x  (= 3) for that to happen. But 
in addition it is reporting two other paths for x = 1 and x =2, despite 
of the fact that there are  only 2 possible paths.

Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the 
path (*temp > 0) is not feasible for any value of x)


Can anybody please give me some insight.

                            int foo(int x, int x1, int x2, int x3, int x4) {
                               int **array = (int **)
                            malloc(4*sizeof(int *));
                               array[0] = &x1;
                               array[1] = &x2;
                               array[2] = &x3;
                               array[3] = &x4;

                               int **ptr = array + x;

                               int* temp =  *ptr;

                               if(*temp > 0) {
                                 assert(1);
                               } else {
                                 assert(0);
                               }
                               return *temp;
                            }


                            int main() {
                               int x;

                               klee_make_symbolic(&x, sizeof(x), "x");
                               klee_assume((x >  0) & (x <  4)); // To
                            allow valid memory access on 'array'
                               return foo(x,10,20,30,-1);
                            }




-- 
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
-------------- next part --------------
HTML attachment scrubbed and removed