[klee-dev] Symbolic output in KLEE

[Cynthia Disenfeld]

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
-------------- next part --------------
HTML attachment scrubbed and removed