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

2016-07-19 Thread 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

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

2016-07-19 Thread Marko Dimjašević
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

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

2016-07-02 Thread Marko Dimjašević
Hi KLEE developers, On Tue, 2016-05-10 at 21:12 -0600, Marko Dimjašević wrote: > I would like to implement support for the Firehose reporting file > format in KLEE: > > https://github.com/fedora-static-analysis/firehose I am close to being done with this one. One will simply add the -firehose-ou

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

2016-05-20 Thread Marko Dimjašević
Hi Martin, On Thu, 2016-05-19 at 15:32 +0200, Martin Nowack wrote: > I guess you want to collect bugs found, > in that case maybe hooking into the test generation function might be a good > idea: > > https://github.com/klee/klee/blob/master/tools/klee/main.cpp#L419 > void KleeHandler::processTe

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

2016-05-19 Thread Martin Nowack
Hi Marko, I guess you want to collect bugs found, in that case maybe hooking into the test generation function might be a good idea: https://github.com/klee/klee/blob/master/tools/klee/main.cpp#L419 void KleeHandler::processTestCase(const ExecutionState &state, const char *errorMessage, const c