[klee-dev] About the two methods of test replay.

[Alex Babushkin]

Hello, I'm sorry if this has ever been asked before, but why are there two
methods for replaying test cases? The first is to link your bitcode file
with the build-generated libraries consisting of functions in instrinsics.c
and so on, and the second one is to use the klee-replay utility. I wonder
whether one of the options is favoured or not, or maybe some option is
to-be-deprecated in the future? Also, is there a guide on how to use the
klee-replay utility properly? klee-replay.c has, for example, the
"klee_make_symbolic" function definition, so, I assume, it is capable of
replaying tests for programs that were instrumented with
"klee_make_symbolic". Yet, klee-replay is mentioned only in the "Testing
Coreutils" guide, in which there is no "klee-make-symbolic" instrumentation
involved. So, how should executables for klee-replay be produced out of
corresponding bitcode files?

Since this is a question about pure usage of the instrument, I'm sorry If
it is a product of bad research of mine. If, however, not, then I think it
would be good to add the appropriate documentation to the klee website.

Thank you for your response in advance, Alex.
-------------- next part --------------
HTML attachment scrubbed and removed