[klee-dev] Implementing support for the Firehose file format

[Martin Nowack]

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ć <marko at 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ć <marko at 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 at 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_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160719/abc93ba8/attachment.sig>