It helps, thanks! On Tue, Feb 2, 2016 at 6:16 PM Cristian Cadar <[email protected]> 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 > > [email protected] > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
