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

[Daniel Guo]

In Executor::getSymbolicSolution function, klee solves the constraints
along a path to generate a representative concrete value for each symbolic
variable.
If you want to get a concrete value at any program point, you can call that
function to grab one for the already visited constraints in current state.

Daniel.

On Mon, Dec 12, 2016 at 4:33 AM, Papapanagiotakis-Bousy, Iason <
iason.papapanagiotakis-bousy.15 at ucl.ac.uk> wrote:

> 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
>
> _______________________________________________
> 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