Hi,
All you need to do is to include your question in the query expression
that is sent to Kleaver. You can find below some documentation about
the structure of query commands in Kleaver:
http://klee.llvm.org/KQuery.html#query_commands
Hope this helps,
Cristian
On 02/15/2012 05:21 AM, ÕÔÏÄ wrote:
> Hello folks:
> I have a problem now, how can I check whether the input data satisfy the
> constraint contained in the .pc file.
> Take the example below
> ///////////Program
> int a;
> klee_make_symbolic(&a, sizeof(a), "input1");
> if(a > 100)
> {
> }
> else
> {
> }
> ///////////////
> run the program with klee, it would generate test000001.pc file looks like
> ///////////////
> array input1[4] : w32 -> w8 = symbolic
> (query [(Eq false
> (Slt 100
> (ReadLSB w32 0 input1)))]
> false)
> /////////////////
> If I get the data 101, how can I check it with test000001.pc to see
> whether 101 satisfy the constraint or not, I think I can use kleaver,
> but I don't know how to use it or modify it.
>
>
> Any information would help me, thank you for your help.
>
> Yours
> XiaZhao
>
>
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
