Hey Marko, This is not that trivial. First, you cannot reexecute klee_init_env() as it currently initialises symbolic file data structure and so on. Second, symbolic and non-symbolic arguments of a program can be interleaved. Maybe, one could factor out the parsing part of klee_init_env() into a separate function which allows you to re-execute it.
Nevertheless, each concretized argument ends up in the `symbolics` attribute of the `ExecutionState` and is named, starting from arg0, arg1, ... You could iterate through that list. `getSymbolicSolution(…, res)` returns a vector of pairs with the first argument the name and the second one the possible assignment of the symbolic. Still, this might be a bit fragile. Hope that helps. Martin > On 19 Jul 2016, at 17:25, Marko Dimjašević <ma...@cs.utah.edu> wrote: > > Hi again, > > On Sat, 2016-07-02 at 20:24 -0600, Marko Dimjašević wrote: >> A thing that I would like to put in the output file is values of input >> arguments to a program for a failing test case when the POSIX runtime >> is used. Usually one calls the klee-replay tool for this. Is there a >> way to use this functionality as a library from within >> tools/klee/main.cpp? > > Does anyone have an answer to this? > > I guess it shouldn't be hard, but I haven't been able to figure it out. > > > -- > Regards, > Marko Dimjašević <ma...@cs.utah.edu> . University of Utah > https://dimjasevic.net/marko . PGP key ID: 1503F0AA > Learn email self-defense! https://emailselfdefense.fsf.org > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev --------------------------------------------------- Martin Nowack Research Assistant Technische Universität Dresden Computer Science Institute of Systems Architecture Systems Engineering 01062 Dresden Phone: +49 351 463 39608 Email: martin_now...@tu-dresden.de ----------------------------------------------------
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
