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

[Dan Liew]

Hi,

On 2 November 2016 at 15:52,  <s.darabi at utwente.nl> wrote:
> 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;

Whilst KLEE is running you can use the `klee_print_expr()` (see
`include/klee/klee.h`) to print the representation of an expression
for debugging purposes. E.g. in example you would do

```
klee_print_expr("ANYTHING", a)
```

However for more complicated programs you should just look at the
generated constraints for each path. You can use
the `-write-smt2s` to write the constraints for each path in SMT-LIBv2
format. You can also use `-write-pcs` to write the constraints
in KLEE's native constraint language.

HTH,
Dan