[klee-dev] Symbolic output in KLEE

[Cynthia Disenfeld]

It helps, thanks!

On Tue, Feb 2, 2016 at 6:16 PM Cristian Cadar <c.cadar at imperial.ac.uk>
wrote:

> 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
> >
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed