[klee-dev] How could I use klee to test big programs?

lyc at seg.nju.edu.cn lyc at seg.nju.edu.cn
Thu Aug 15 14:56:11 BST 2013


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





More information about the klee-dev mailing list