Dear Klee developers,
I am trying to use Klee for specification generation. To do that I need Klee's
intermediate symbolic results. Specifically, I need the guards of each path in
the program to be printed in their symbolic forms. For example, in the
following program:
get_sign(int a,char * sign)
{
if (a==0) *sign = 0;
else if (a<0) *sign = -1;
else *sign = 1;
}
I want,
Path1 : (a==0)
Path2 : (a<0)
Path3: (a>0)
as output and if it is possible to have the value of sign or the range of sign
value for each path.
Path1: (a==0)==> *sign = 0;
Path2: (a<0)==> *sign = -1;
Path3: (a>0)==> *sign = 1;
Questions:
?Is there any Klee command line option that can activate any symbolic output?
If yes please refer me to its manual page.
If no, can Klee basically be extended to generate such an output?
Thanks in advance,
Saeed Darabi
?
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
