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
