Hi,
On 2 November 2016 at 15:52, <[email protected]> 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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
