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

[Cristian Cadar]

I only had a brief look at your code, but it looks like you are storing 
the addresses of the x_i variables into the array, which is likely not 
what you intended.

Cristian

On 18/12/13 06:39, Sandeep wrote:
> 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>