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
