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

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>