See http://www.mail-archive.com/[email protected]/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 <[email protected]
<mailto:[email protected]>>
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
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
