[klee-dev] Compiling a whole application

Tom Ritter tom at ritter.vg
Sat May 16 05:24:58 BST 2015


Hi all,

I think this is a common problem, but I'm having difficulty building a
whole application for testing with klee.

I tried a couple of approaches, and have wound up with a mess of
tools.  These include:
 - the llvm-gcc 2.9 binary distribution
 - llvm 2.9 built from source (first without, then with, clang 2.9)
 - wllvm
 - wllvm with llvm-gcc support


I've tried the following to get a couple of
complex-but-not-too-complex projects:

 - klee-gcc (the wrapper script they wrote) seems to be admittedly inadequate.
It doesn't produce binary files, so configure scripts that check to
make sure the compiler works fails

 - the wllvm fork at [1] using llvm-gcc ends up failing with __FD
errors I can't track down:
undefined reference to `__FDELT'
undefined reference to `__FDMASK'

 - vanilla wllvm at [0] using clang (from my 2.9 llvm folder) ends up
failing with
/usr/bin/ld: cannot find crt1.o: No such file or directory
/usr/bin/ld: cannot find crti.o: No such file or directory
/usr/bin/ld: cannot find crtbegin.o: No such file or directory
/usr/bin/ld: cannot find -lgcc
/usr/bin/ld: cannot find -lgcc_s

I fixed the first two missing crt files for the llvm-gcc case by
symlinking: /home/tom/klee/llvm-gcc4.2-2.9-x86_64-linux/lib/gcc/x86_64-unknown-linux-gnu/4.2.1/crt1.o
-> /usr/lib/x86_64-linux-gnu/crt1.o
But I can't A) figure out where to put the symlinks for this version
of wllvm and B) can't find crtbegin.o

-tom

[0] https://github.com/travitch/whole-program-llvm
[1] https://github.com/delcypher/whole-program-llvm/tree/llvm-gcc



More information about the klee-dev mailing list