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