[klee-dev] Complete Input with klee

[ANAS faruqui]

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 <urrimus at hotmail.com>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: 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