[klee-dev] Print out intermediate symbolic representation for each path instead on generating test-case for each path

[s.darabi at utwente.nl]

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

?




-------------- next part --------------
HTML attachment scrubbed and removed