Hi Jason, What you want can be achieved by using concolic execution or using seed mode in KLEE. The default mode of KLEE is symbolic execution. For concolic execution, you can try ZESTI or S2E. For seed mode in KLEE, you need somehow convert your concrete input to a .ktest file so KLEE can read it.
The two approaches you tried should not work. First approach will result in a constraint Phi ^ (x==value) where Phi is the path constraints so the result is always x=value as you got or unsatisfiable. The second one also does not work because by writing a concrete value to a symbolic variable, you will write concrete value to the memory area allocated for this variable in the symbolic memory model of KLEE -> that memory area will not be symbolic anymore, it is concrete. Hope it will helps, Thuan On Mon, Dec 12, 2016 at 8:33 PM, 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
