You can use the klee_print_expr intrinsic to print symbolic expressions.
Cristian
On 02/02/2016 18:34, Cynthia Disenfeld wrote:
Hi,
I have recently installed KLEE and I was wondering whether it is
possible to obtain the symbolic output. For example, given the following
variation of the get_sign function:
if (x == 0)
return 0;
if (x < 0)
return x-1;
else
return x+1;
Is there any log / parameter/ command with which I could automatically
obtain:
For the path constraints ((x==0)) the output is (0)
For the path constraints (!(x==0) && (x<0)) the output is (x-1)
For the path constraints (!(x==0) && (x>0)) the output is (x+1)
So far, I have observed that it is possible to get the smt constraints
of the input, or use the automatic tests generated and get the output,
but this is a concrete value and not the path's symbolic output.
Thanks,
Cynthia Disenfeld
_______________________________________________
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
