[klee-dev] About klee's detection problems in real software

rongze xv xxurongze at gmail.com
Tue Sep 15 04:30:44 BST 2020


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
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list