Getting Started: Building and Running KLEE

Building KLEE and Working with the Code

If you would like to try KLEE, the current procedure for building is below.

KLEE is built on LLVM; the first steps are to get a working LLVM installation. See Getting Started with the LLVM System for more information.

NOTE: KLEE is only currently tested on Linux and Darwin x86-32 targets, using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g., 2.5), and is currently untested on any x86-64 target, although we hope to add support for them soon.

1. Install llvm-gcc:
• Download and install the LLVM 2.5 release of llvm-gcc from here. Add llvm-gcc to your PATH. It is important to do this first so that llvm-gcc is found in subsequent configure steps. llvm-gcc will be used later to compile programs that KLEE can execute.
2. Checkout and build LLVM from SVN head (LLVM 2.5 will not work):
   svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm
   cd llvm
   ./configure --enable-optimized
   make
   (the --enable-optimized configure argument is not necessary, but KLEE runs very slowly in Debug mode).
3. Checkout KLEE (to any path you like):
   svn co http://llvm.org/svn/llvm-project/klee/trunk klee
4. Configure KLEE (from the KLEE source directory):
   ./configure --with-llvm=path/to/llvm

   This assumes that you compiled LLVM in-place. If you used a different directory for the object files then use:

   ./configure --with-llvmsrc=path/to/llvm/src --with-llvmobj=path/to/llvm/obj
5. Build KLEE (from the KLEE source directory):
   make ENABLE_OPTIMIZED=1
6. Run the regression suite to verify your build:
   make check
   make unittests
   
7. You're ready to go! Go to the Tutorials page to try KLEE.