Hi,
Yes, you need to compile the system under test to LLVM bitcode.
However, nowadays things are much easier with the use of wllvm, as
illustrated in that tutorial.
Regarding the error you mentioned, just look in the .external.err file,
it should contain an explanation about the issue.
Best,
Cristian
On 15/09/2020 04:30, rongze xv wrote:
Hi all，
I am a graduate student, my name is Xu Rongze. I recently read your
paper "KLEE: Unassisted and Automatic Generation of High-Coverage Tests
for Complex Systems Programs", and learn how to use KLEE. I saw the
tutorial on the official website: "Testing Coreutils" clearly stated
"One of the difficult parts of testing real software using KLEE is that
it must be first compiled so that the final program is an LLVM bitcode
file and not a native binary. " I think this means that when I use KLEE
to test real software, I need to build the environment for each real
software? If I test a function level code in a project, do I need to
write the corresponding driver, or do I need to write only one driver
for a project?
When I tested in coreutils, I tested the echo.bc file separately
according to the tutorial and there was no problem, but I tested other
files separately, such as tr.bc, and an error (external.err) occurred. I
don't know the reason. Is it related to the driver?
If you can reply to me in your spare time, thank you very much!!
Sincerely，
Xu Rongze
_______________________________________________
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
