[klee-dev] How can I get the testcase content in real-time?

Frank Busse f.busse at imperial.ac.uk
Wed Dec 8 11:07:04 GMT 2021


Hi,


On Wed, 8 Dec 2021 16:14:13 +0800
rongze xv <xxurongze at gmail.com> wrote:

> If I understand correctly, the state of KLEE should represent the
> currently running path? If this is the case, KLEE will generate a test
> case for each state. I hope that when KLEE generates each test case,
> its test case content will be output in real-time. Which part of the
> code should be modified (I guess it is in the run function of
> Executor. cpp)? Or is there an easier way to change it?

Not sure what you want. KLEE writes test cases at the end of a path,
either when an error was found or a state got killed/early terminated.
Do you want to write test cases earlier or do you want to output the
data in a different format?


Kind regards,

Frank



More information about the klee-dev mailing list