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

[Pablo González de Aledo]

I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.

May be the next code is simpler, and still explains the issue.

int main() {
int a;
int array[] = {1,2,3,4,5};

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

if(array[a] == 3)
return 0;
else
 return 1;
}

Why does Klee generate 17 solutions when only one is possible (a == 2) ?

Thanks.



2014/1/7 Cristian Cadar <c.cadar at imperial.ac.uk>

> 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
>>
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed