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
