On 22/12/2022 16:09, Muralee, Siddharth wrote:
Hello,
I am currently working on a project to verify states that end due to
errors such as "memory error: out of bound pointer". Currently, I am
trying to extract some information about these states, and the most
information I am able to extract is the instruction log from replaying
only the seed file, using the options |--debug-print-instructions| and
|--only-seed --seed-file| .
Is there any way to extract more details? While running an application
with a seed input.
What other info would you like? Most likely you would need to add
support for additional info yourself.
Also, for the |debug-print-instructions=all:stderr| is there any way to
restrict Klee from printing all the instructions inside the libraries?
It takes an insane amount of time looping inside the runtime setup code
as well as library functions such as sprintf etc.
There are no options to do so, but this could be easily accomplished by
changing the code.
To reduce the amount of logged data, you could use
--debug-compress-instructions, which compresses the logged instructions
in gzip format.
Best,
Cristian
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
