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

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>