[klee-dev] Choosing the concrete values and getting the symbolic constraints

[Papapanagiotakis-Bousy, Iason]

Hi everyone,


I would like to know how could I specify the concrete values chosen by KLEE to execute.

Instead of the normal mode of KLEE I would like to be able to choose a value (I am interested only in integers and assume for simplification that there is only one symbolic variable in the program) and execute the program in KLEE with that value and record the symbolic constraints encountered.


I've tried the following two approaches:
1) using klee_assume(x==the_value_of_my_choice)

this does not seem to work as the only constraint that is generated in kquery is the one I've given to klee_assume.


2) assigning a value to the symbolic variable

int x;

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

x=the_value_of_my_choice

this does not seem to work either as the resulting kquery file has an empty query "(query [] false)".


How could I pick the value used during concolic execution and get the symbolic constraints?


Thank you in advance for your suggestions.


Best regards,

Jason
-------------- next part --------------
HTML attachment scrubbed and removed