Hi Alex,
I noticed this email went unanswered, hopefully the response is still
useful. In short, we plan to maintain both replay methods. As you
point out, the klee-replay tool only works when there are no klee_
intrinsics in the code. In this case, it is the preferred method, as
it's easier to use, you just need the native binary and a ktest file.
The other method is more general, but a bit more difficult to use.
Best,
Cristian
On 05/04/2021 21:46, Alex Babushkin wrote:
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.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
