Update Oct 2014:
The original installation log was written in June 2013. At that time Klee project was hosted on http://klee.llvm.org, and their installation instruction was quite confused. Now they move the project to http://klee.github.io/.
It looks like that they have completely re-written the installation instructions on the new website, the procedure is very similar to the one I logged below, you can also refer to their official tutorial.
I was trying to set up KLEE on Ubuntu 13.04 x64 server edition based on official KLEE guide: http://klee.llvm.org/GetStarted.html.
llvm-gcc and llvm 2.9 are necessary to KLEE. Initially I tried to compile llvm-gcc from source code on my server, but it failed for some reason. I didn’t have time digging into it (error message is very similar to another user’s post at http://s1151.socode.info/question/508146694f1eba38a44c48e6) So I just use a binary version of llvm-gcc during my installation.
Notice I also use a text editor to edit one of the .cpp files (see comment in the code below) to avoid an error while compiling. I use ‘make -j ‘ to compile faster (if errors occur, please only use ‘make’).
#XL @ 2013.6.29 $ sudo apt-get install build-essential #Install dependencies $ sudo apt-get install g++ curl dejagnu subversion bison flex #download llvm-gcc, I put it in home folder $ cd ~ $ sudo curl -O http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 $ tar xjvf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 #add path $ echo "export PATH=$PATH:~/llvm-gcc4.2-2.9-x86_64-linux/bin" >> ~/.bashrc $ echo "export PATH=$PATH:~/klee/Release+Asserts/bin" >> ~/.bashrc $ echo "export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" >> ~/.bashrc $ source ~/.bashrc #download and install llvm $ sudo curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz $ tar zxvf llvm-2.9.tgz $ cd llvm-2.9 $ ./configure --enable-optimized --enable-assertions $ vi ~/llvm-2.9/lib/ExecutionEngine/JIT/Intercept.cpp # Use vi (or other text editor) to add this line # at the beginning of this cpp file: #include “unistd.h” # Otherwise the compiling process may fail $ make -j $(grep -c processor /proc/cpuinfo) $ cd .. $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp $ cd stp $ ./scripts/configure --with-prefix=/home/$(whoami)/stp_install --with-cryptominisat2 $ make -j $(grep -c processor /proc/cpuinfo) OPTIMIZE=-O2 CFLAGS_M32= install $ cd .. $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee $ cd klee $ ./configure --with-llvm=/home/$(whoami)/llvm-2.9 --with-stp=/home/$(whoami)/stp_install $ make -j $(grep -c processor /proc/cpuinfo) ENABLE_OPTIMIZED=1 $ make unittests