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-output command line argument to KLEE and it will generate firehose.xml in the klee-last directory. 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? An attempt I made is to simply read from m_argv in the KleeHandler class, but that doesn't work if there are symbolic inputs to the program (e.g., I obtain things like "--sym-arg 3" instead of a concrete value that lead to the failure). Then there is Executor::getSymbolicSolution, which is probably related, but I don't know how to make the solution concrete. My hunch is I'd maybe have to call the klee_init_env function from runtime/POSIX/klee_init_env.c. However, I've been wondering if it's safe to do so from the KleeHandler::processTestCase function in tools/klee/main.cpp. In other words, does klee_init_env impact a global state and does it have side-effects? If I should do something else to obtain concrete input values, I will be more than happy to hear your suggestion. -- 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
signature.asc
Description: This is a digitally signed message part
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev