[klee-dev] About TestComp-specific KLEE command-line options.

2023-06-16 Thread Alex Babushkin
Hello, In the KLEE Wrapper used for TestComp there are some command-line options that are not present in the KLEE repository. The following options are missing: -write-xml-tests -tc-orig -tc-hash --tc-type -dump-test-case-type -coverage-on-the-fly The first three are present in the following

[klee-dev] On how the standard library is linked.

2022-11-03 Thread Alex Babushkin
Hello. KLEE can call functions that do not have IR available as externals. Some C standard library functions are also called as externals (e.g. printf). How is the standard library linked to the JIT engine that calls externals? Also, why isn't loading of binary-only libraries supported in KLEE?

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

2021-04-05 Thread 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

[klee-dev] XML test format for TestComp.

2020-12-01 Thread Alex Babushkin
Hello. In the archive of TestComp 2020 I found a KLEE submission. There I found a python script for compiling and executing verification tasks. There KLEE seems to have an option called '-write-xml-tests', which is not currently present in the release version. Was it removed or renamed? If it was