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
