[klee-dev] Symbolic output in KLEE

[Cristian Cadar]

You can use the klee_print_expr intrinsic to print symbolic expressions.

Cristian

On 02/02/2016 18:34, Cynthia Disenfeld wrote:
> Hi,
>
> I have recently installed KLEE and I was wondering whether it is
> possible to obtain the symbolic output. For example, given the following
> variation of the get_sign function:
>
>
>    if (x == 0)
>
>      return 0;
>
>
>    if (x < 0)
>
>      return x-1;
>
>    else
>
>      return x+1;
>
>
> Is there any log / parameter/ command with which I could automatically
> obtain:
>
> For the path constraints ((x==0)) the output is (0)
>
> For the path constraints (!(x==0) && (x<0)) the output is (x-1)
>
> For the path constraints (!(x==0) && (x>0)) the output is (x+1)
>
>
> So far, I have observed that it is possible to get the smt constraints
> of the input, or use the automatic tests generated and get the output,
> but this is a concrete value and not the path's symbolic output.
>
>
> Thanks,
>
> Cynthia Disenfeld
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>