[klee-dev] Complete Input with klee

[Urmas Repinski]

Hi, Anas.

Exactly, klee_assume(false) means that every path, that will contain this statement, will not be processed. So if there is condition, as example a==5, when this path is reached, then a=5 will be never generated, same is with b==5 and c==5, that is equivalent to klee_assume(a != 5 & b != 5 & c !=5).

klee_assume(true) does not mean anything, this statement will be executed when it will be reached, so if you just want to have some additional condition for input generation, like

if(a==5)klee_assume(true);
then probably a<5, a=5, and a>5 will be generated. This is useful if you want to add some instrumentations or conditions for the generated variable's values. I did some work with klee in this direction actually, but without any meaningful results unfortunately, but you can try too if you want.

klee_assert() is probably is the same as C assert() function, but implemented using klee. It will catch error when assertion will fail - (http://ccadar.github.io/klee/Tutorial-2.html, assert: An assertion failed.) and print it during test generation, to  testN.TYPE.err file.

With best wishes,
Urmas. 


From: anas.faruqui at gmail.com
Date: Mon, 28 Oct 2013 12:17:03 -0400
Subject: Re: [klee-dev] Complete Input with klee
To: urrimus at hotmail.com
CC: klee-dev at imperial.ac.uk; loi.luuthe at gmail.com

So if a condition has klee_assume(false) just after it, then would this mean that klee will not take that path  (or if it has klee_assume(true) then it would not take the other path.)
can someone tell me more about klee_assume() and klee_assert().


Thanks

On Mon, Oct 28, 2013 at 11:55 AM, Urmas Repinski <urrimus at hotmail.com> wrote:





Hi,

Using same analogy you can use klee_assume(false);

So  klee_assume(a != 5 & b != 5 & c !=5) breaks the path when a==5 || b==5 || c==5, when condition is false, then klee_assume(false); will get all paths, that reached the klee_assume location, so using 


klee_assume(a != 5 & b != 5 & c !=5)  is same as to use

int a, b, c;
if(a==5)klee_assume(false);
if (b==5)
klee_assume(false);

if (c==5)klee_assume(false);
printf("success")'
Second one is possibly what you need.

Urmas Repinski.

From: anas.faruqui at gmail.com


Date: Mon, 28 Oct 2013 11:29:48 -0400
To: loi.luuthe at gmail.com
CC: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Complete Input with klee



Thanks for your reply.
i am looking for a way where i can guide a condition to be always true or false. Is there a way through which i can tell klee to do that?





On Mon, Oct 28, 2013 at 12:20 AM, Loi Luu <loi.luuthe at gmail.com> wrote:




So I think you want something like klee_assume(a != 5 & b != 5 & c !5)
Thanks,

On Mon, Oct 28, 2013 at 12:06 PM, ANAS faruqui <anas.faruqui at gmail.com> wrote:





Hello all,
I want klee to output only the complete inputs and do not take the early termination paths. 





For example : if we have a code as following


int a, b, c;
if(a==5)exit(1);
if (b==5)exit(1);
if (c==5)exit(1);
printf("success")'







KLEE gives me many cases which include a or b or c = 5.
What changes can i do (in KLEE   or in the code) so that it will only output cases which would contain all a, b, c, !=5.







In other words can I force klee to make a condition always false or true?

thanks

_______________________________________________

klee-dev mailing list

klee-dev at imperial.ac.uk

https://mailman.ic.ac.uk/mailman/listinfo/klee-dev




-- 





Loi, Luu The (Mr.)RA at Security Lab, SoC, NUS





_______________________________________________
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