KLEE configuration error

Question

I am trying to install KLEE by following the step at:

http://klee.github.io/getting-started/

Unfortunately, at step 06 "Configure KLEE: From the KLEE source directory, run:"

I get the following error:

xxx@xxx18:~/klee$ ./configure --with-llvm=/home/xxx/llvm-2.9 --with-stp=/home/xxx/stp-r940/install
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking for g++... g++
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking target system type... x86_64-unknown-linux-gnu
checking type of operating system we're going to host on... 
checking llvm source dir... /home/xxx/llvm-2.9
checking llvm obj dir... /home/xxx/llvm-2.9
checking llvm package version... 2.9
checking llvm version major... 2
checking llvm version minor... 9
checking llvm is release version... 1
checking if LLVM needs C++11... no
checking llvm build mode... Release+Asserts
checking llvm has asserts enabled... 1
checking LLVM Bitcode compiler... 
checking for llvm-gcc... FOUND
checking for llvm-g++... FOUND
Using C llvm compiler : /usr/bin/llvm-gcc
Using C++ llvm compiler : /usr/bin/llvm-g++
checking C LLVM Bitcode compiler works... Potential incompatible plugin version. GCC: 4.6 (20120301). Expected: 4.6 (20120301)
Defines 'dragonegg_disable_version_check' as env variable to remove this warning
Please note that unexpected errors might occur.
/home/xxx/llvm-2.9/Release+Asserts/bin/llvm-dis: Invalid bitcode signature
configure: error: Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?

Does anyone had same issue?

Thanks

Giuseppe

Answer 1

I coded up this configure check. It is checking that the compiler detected for creating LLVM bitcode can create LLVM bitcode that works with the version of LLVM that KLEE is being built against. If this check didn't exist and there is bitcode incompatibility then compilation of KLEE's runtime would later fail so this tries to detect the failure earlier.

It looks like /usr/bin/llvm-gcc isn't generating LLVM bitcode that works with the version of LLVM you're compiling against. You will need to debug this yourself. You can take a look at the autoconf/configure.ac file to see how the check is implemented.

As already suggest a great way to get started without all this hassle is our Docker image