Re: [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,   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
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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

[s.darabi]

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