Hi Urmas, Thanks much for the detailed answer.
I tried using klee_assume(false). but at the time of compilation it says false in not defined. I used FALSE as well with the same error. The i just have used 0 as the parameter. This compiled perfectly. But when klee runs, it prints the error saying invalid klee_assume call (provably false) KLEE: NOTE: now ignoring this error at this location But KLEE is still generating incomplete test cases. Could it be because of the fact that the call to klee_assume is ignored? Thanks On Mon, Oct 28, 2013 at 12:29 PM, Urmas Repinski <[email protected]>wrote: > 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 test*N*.*TYPE*.err file. > > With best wishes, > Urmas. > > > ------------------------------ > From: [email protected] > Date: Mon, 28 Oct 2013 12:17:03 -0400 > > Subject: Re: [klee-dev] Complete Input with klee > To: [email protected] > CC: [email protected]; [email protected] > > > 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 <[email protected]>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: [email protected] > Date: Mon, 28 Oct 2013 11:29:48 -0400 > To: [email protected] > CC: [email protected] > 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 <[email protected]> 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 <[email protected]>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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > > -- > Loi, Luu The (Mr.) > RA at Security Lab, SoC, NUS > > > > _______________________________________________ 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
