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 < [email protected]> 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 > [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
