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

[Cristian Cadar]

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