Hi Kirill,
KLEE does not perform any kind of abstraction for loops. In your
example, the order in which paths are explored is dictated by the search
heuristics employed.
Cristian
On 25/03/14 09:33, Kirill Bogdanov wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
