Hello All,
I am trying to understand how KLEE symbolically executes a loop.
For that, I tried out with the following example,
int main() {
int i = 3 , N, sum = 0 ;
klee_make_symbolic(&N, sizeof(N), "N");
klee_assume(N > 1 & N < 10);
for(i= 3 ; i< N; i++) {
}
return sum;
}
I am getting 7 values for symbolic variable N (value '2' for loop exit
and values '4, 5, 6, 7, 8, 9' for paths inside the loop).
I think what is happening here is:
For each iteration of the loop a path condition is generated like (3 < N
for 1st iteration and 4 < N for the 2nd and soon) and KLEE is solving
all of them.
Also it is solving for 3 >=N for the loop exit.
Please let me know if my understanding is correct.
If this is correct, then
With the following code,
int main() {
int i , N=10 ;
klee_make_symbolic(&i, sizeof(i), "i");
klee_assume(i > -1);
for( ; i< N; i++) {
}
return i;
}
I am getting 11 generated tests (10 testcases with i values 0, 1, 2,
..., 9) for paths in the loop and 1 for the loop exit.
My question is how KLEE is working here. And how the path conditions are
generated.
If my previous assumption is true, then it must work like:
For each iteration of the loop a different path condition is generated
(like i < N for 1st and 2*i < N and soon ) and if that be the case then the
conditions to be inside the loop will be 5 in number like i < 10, i < 5
; i < 3 ; i < 2 and i < 1.
But why we are getting 9 testcases as paths inside the loop. Please explain.
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
University Of Illinois Urbana Champaign.
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
