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

[Cristian Cadar]

See http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00891.html

Cristian

On 07/01/14 18:26, Pablo González de Aledo wrote:
> 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
> <mailto: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 <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>         <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>     _________________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>     <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
>