How to deal with loop?

[Sandeep Dasgupta]

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.