[klee-dev] Symbolic output for each branch

[Alexander Tough]

Hi,


#include<klee/klee.h>


int seven_plus(int x)

{

if(x>10)

return x;

else

return 7+x;

}


int main()

{

int a;

klee_make_symbolic(&a,sizeof(a),"a");

return seven_plus(a);

}

If I wanted to obtain the symbolic "return values" for each path (i.e. "a" for the "x>10" branch and 7+"a" for the "else" branch), where would I start? I was thinking of assigning the return value to a dummy variable "y" and then use klee_print_expr("y=",y), but I wonder if there is a way to do this without altering the source program.

Thanks,

Alex Tough
-------------- next part --------------
HTML attachment scrubbed and removed