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

[Urmas Repinski]

Hi, Kirill.

First of all, it is not clear what type of inputs should be generated.
In the example below all integers will be generated, starting from 0 ... including 500. 
klee_assert function will trigger __assert_fail klee function, this possibly will terminate input generation process, possibly not, i am not very sure.

Anyway it is possible that you want something more meaningful, if input 500 should be generated, or input 500 should not be generated.

In this case better to use klee_assume function:

 void klee_assume(int constraint) {
  
if (!constraint) klee_silent_exit(0);

}


{int a;
klee_make_symbolic(&a, sizeof(a), "a");
int i =0 ;
int n =1;
for (i =0; i < a;i++){

n++;
}
klee_assume(n==500); or klee_assume(n!=500);
Will generate a=500 or all a-s, except 500.

Urmas Repinski.

Date: Tue, 25 Mar 2014 09:33:26 +0000
From: kirill.sc at gmail.com
To: klee-dev at imperial.ac.uk
Subject: [klee-dev] KLEE relationship between loop length and counter.

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 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed