[klee-dev] KLEE relationship between loop length and counter.

[Kirill Bogdanov]

Hello Everyone,
(Sorry for the previous email, it has been sent by mistake before I
finished it!)

Could you please let me know if what I am doing cannot be achieved with
KLEE and if it can, how can I do it?

1. Please consider my usage example below. The problem that I am observing
is that KLEE does not sees relationship between loop length and the counter
"n".
In my experiments (with different search strategies) KLEE always
encountered assertion by a blind search, and usually after generating 500
test cases.

{
int a;
klee_make_symbolic(&a, sizeof(a), "a");
int i =0 ;
int n =1;
for (i =0; i < a;i++){
n++;
}
if (n == 500)
klee_assert(0);
return 0;
}

Is this is something that is fundamentally impossible in KLEE, or can be
achieved by rewriting my example?


Thank you very much!
-------------- next part --------------
HTML attachment scrubbed and removed