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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
