Hi, Anas. I suggest to use --emit-all-errors
option, this should disable error's warnings, and probably when this parameter is on the klee execution will continue, but i am not really sure, i had never used klee_assume(false); actually, only klee_assume(true); Read detailed parameter's description in klee help (klee -h), the klee is not installed on my system, so i cant help you with that. You are welcome, Urmas. From: [email protected] Date: Mon, 28 Oct 2013 18:45:40 -0400 Subject: Re: [klee-dev] Complete Input with klee To: [email protected] CC: [email protected] 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 testN.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
