How could I use klee to test big programs?

[l***@public.gmane.org]

Hi there,
This is the first time I post to this mailing list but the question I
will illustrate following has been bothering me for very a long time.
Klee is built on llvm, so the very first step to make things going is
compiling the programs into llvm bitcode with llvm compiler. I did as
the tutorial( http://ccadar.github.io/klee/Tutorials.html) said and
used llvm-gcc to compile the programs that I wanted them to be fed into
klee. It is easy to do so with programs with single source file, but
things become difficult when the program is big. Especially for
real-world open source programs like openssl, texinfo and so on, it is
not an easy job to build the things with llvm. Mr. Cadar and his
workmates built coreutil successfully using klee-gcc which is a script
written by them. However, not everything can be settled down by a
simple script to hack the shell.

So I am writing this mail to ask for your opinions or experiences on how
to really run big programs(like openssl, texinfo) with klee.

It would be highly appreciated if I could receive your replies.


Thanks and best wishes,
Ben Li

[Kuchta, Tomasz]

Hello,
I came across the following script:

https://github.com/travitch/whole-program-llvm

Unfortunately, I am unable to tell whether it will work for openssl or texinfo.
I thought that maybe it will be useful for you.

Best regards,
Tomek Kuchta

Post by l***@public.gmane.org
Hi there,
This is the first time I post to this mailing list but the question I
will illustrate following has been bothering me for very a long time.
Klee is built on llvm, so the very first step to make things going is
compiling the programs into llvm bitcode with llvm compiler. I did as
the tutorial( http://ccadar.github.io/klee/Tutorials.html) said and
used llvm-gcc to compile the programs that I wanted them to be fed into
klee. It is easy to do so with programs with single source file, but
things become difficult when the program is big. Especially for
real-world open source programs like openssl, texinfo and so on, it is
not an easy job to build the things with llvm. Mr. Cadar and his
workmates built coreutil successfully using klee-gcc which is a script
written by them. However, not everything can be settled down by a
simple script to hack the shell.
So I am writing this mail to ask for your opinions or experiences on how
to really run big programs(like openssl, texinfo) with klee.
It would be highly appreciated if I could receive your replies.
Thanks and best wishes,
Ben Li
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev