Implement a CMake based build system for KLEE.

This is based off intial work by @jirislaby in #481. However it
has been substantially modified.

Notably it includes a separate build sytem to build the runtimes which
is inspired by the old build system. The reason for doing this is
because CMake is not well suited for building the runtime:

* CMake is configured to use the host compiler, not the bitcode
  compiler. These are not the same thing.

* Building the runtime using `add_custom_command()` is flawed
  because we can't automatically get transitive depencies (i.e.
  header file dependencies) unless the CMake generator is makefiles.
  (See `IMPLICIT_DEPENDS` of `add_custom_command()` in CMake).

So for now we have a very simple build system for building the runtimes.
In the future we can replace this with something more sophisticated if
we need it.

Support for all features of the old build system are implemented apart
from recording the git revision and showing it in the output of
`klee --help`.

Another notable change is the CMake build system works much better with
LLVM installs which don't ship with testing tools. The build system
will download the sources for `FileCheck` and `not` tools if the
corresponding binaries aren't available and will build them. However
`lit` (availabe via `pip install lit`) and GTest must already be
installed.

Apart from better support for testing a significant advantage of the
new CMake build system compared to the existing "Autoconf/Makefile"
build system is that it is **not** coupled to LLVM's build system
(unlike the existing build system). This means that LLVM's
autoconf/Makefiles don't need to be installed somewhere on the system.

Currently all tests pass.

Support has been implemented in TravisCI and the Dockerfile for
building with CMake.

The existing "Autoconf/Makefile" build system has been left intact
and so both build systems can coexist for a short while. We should
remove the old build system as soon as possible though because it
creates an unnecessary maintance burden.

53 files changed, 2835 insertions, 91 deletions

diff --git a/.travis.yml b/.travis.yml
index 5c7adeed..060f4d0f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -30,6 +30,11 @@ env:
     # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set
 
     matrix:
+    # Check KLEE CMake build
+    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
+    - LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
+
     # Test experimental metaSMT support
     - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
     - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -63,7 +68,6 @@ env:
     # Check with TCMALLOC
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
     - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-
     global:
     - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
     - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 98dbbc0d..64bfcb67 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -34,10 +34,18 @@ if [ "${KLEE_UCLIBC}" != "0" ]; then
     cd klee-uclibc
     ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION}
     make
-    KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime"
+    if [ "X${USE_CMAKE}" == "X1" ]; then
+      KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE"
+    else
+      KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime"
+    fi
     cd ../
 else
-    KLEE_UCLIBC_CONFIGURE_OPTION=""
+    if [ "X${USE_CMAKE}" == "X1" ]; then
+      KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE"
+    else
+      KLEE_UCLIBC_CONFIGURE_OPTION=""
+    fi
 fi
 
 COVERAGE_FLAGS=""
@@ -54,52 +62,110 @@ KLEE_STP_CONFIGURE_OPTION=""
 KLEE_METASMT_CONFIGURE_OPTION=""
 SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
 
-for solver in ${SOLVER_LIST}; do
-  echo "Setting configuration option for ${solver}"
-  case ${solver} in
-  STP)
-    KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build"
-    ;;
-  Z3)
-    echo "Z3"
-    KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr"
-    ;;
-  metaSMT)
-    echo "metaSMT"
-    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}"
-    ;;
-  *)
-    echo "Unknown solver ${solver}"
-    exit 1
-  esac
-done
-
+if [ "X${USE_CMAKE}" == "X1" ]; then
+  # Set CMake configure options
+  for solver in ${SOLVER_LIST}; do
+    echo "Setting CMake configuration option for ${solver}"
+    case ${solver} in
+    STP)
+      KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build"
+      ;;
+    Z3)
+      echo "Z3"
+      KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE"
+      ;;
+    metaSMT)
+      echo "metaSMT"
+      if [ "X${METASMT_DEFAULT}" == "X" ]; then
+        METASMT_DEFAULT=STP
+      fi
+      KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}"
+      ;;
+    *)
+      echo "Unknown solver ${solver}"
+      exit 1
+    esac
+  done
+  TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
+else
+  for solver in ${SOLVER_LIST}; do
+    echo "Setting configuration option for ${solver}"
+    case ${solver} in
+    STP)
+      KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build"
+      ;;
+    Z3)
+      echo "Z3"
+      KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr"
+      ;;
+    metaSMT)
+      echo "metaSMT"
+      KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}"
+      ;;
+    *)
+      echo "Unknown solver ${solver}"
+      exit 1
+    esac
+  done
+
+  TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc")
+fi
 
-TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc")
 ###############################################################################
 # KLEE
 ###############################################################################
 mkdir klee
 cd klee
 
-# Build KLEE
-# Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged
-# and is missing the shared library that was supposed to be built that the build
-# system will try to use by default.
-${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \
-            --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \
-            --with-llvmcc=${KLEE_CC} \
-            --with-llvmcxx=${KLEE_CXX} \
-            ${KLEE_STP_CONFIGURE_OPTION} \
-            ${KLEE_Z3_CONFIGURE_OPTION} \
-            ${KLEE_METASMT_CONFIGURE_OPTION} \
-            ${KLEE_UCLIBC_CONFIGURE_OPTION} \
-            ${TCMALLOC_OPTION} \
-            CXXFLAGS="${COVERAGE_FLAGS}" \
-            && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-                    ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-                    ENABLE_SHARED=0
-
+if [ "X${USE_CMAKE}" == "X1" ]; then
+  GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/"
+  if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
+    KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE"
+  else
+    KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE"
+  fi
+
+  if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
+    CMAKE_BUILD_TYPE="RelWithDebInfo"
+  else
+    CMAKE_BUILD_TYPE="Debug"
+  fi
+  # Compute CMake build type
+  CXXFLAGS="${COVERAGE_FLAGS}" \
+  cmake \
+    -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \
+    -DLLVMCC="${KLEE_CC}" \
+    -DLLVMCXX="${KLEE_CXX}" \
+    ${KLEE_STP_CONFIGURE_OPTION} \
+    ${KLEE_Z3_CONFIGURE_OPTION} \
+    ${KLEE_METASMT_CONFIGURE_OPTION} \
+    ${KLEE_UCLIBC_CONFIGURE_OPTION} \
+    ${TCMALLOC_OPTION} \
+    -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
+    -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
+    ${KLEE_ASSERTS_OPTION} \
+    -DENABLE_TESTS=TRUE \
+    -DLIT_ARGS="-v" \
+    ${KLEE_SRC} && make
+else
+  # Build KLEE
+  # Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged
+  # and is missing the shared library that was supposed to be built that the build
+  # system will try to use by default.
+  ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \
+              --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \
+              --with-llvmcc=${KLEE_CC} \
+              --with-llvmcxx=${KLEE_CXX} \
+              ${KLEE_STP_CONFIGURE_OPTION} \
+              ${KLEE_Z3_CONFIGURE_OPTION} \
+              ${KLEE_METASMT_CONFIGURE_OPTION} \
+              ${KLEE_UCLIBC_CONFIGURE_OPTION} \
+              ${TCMALLOC_OPTION} \
+              CXXFLAGS="${COVERAGE_FLAGS}" \
+              && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
+                      ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
+                      ENABLE_SHARED=0
+fi
 ###############################################################################
 # Testing
 ###############################################################################
@@ -108,32 +174,42 @@ set +e # We want to let all the tests run before we exit
 ###############################################################################
 # Unit tests
 ###############################################################################
-# The unittests makefile doesn't seem to have been packaged so get it from SVN
-sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/
-svn export  http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \
-    ../Makefile.unittest
-sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/
-
-make unittests \
-    DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-    ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-    ENABLE_SHARED=0
-RETURN="$?"
+if [ "X${USE_CMAKE}" == "X1" ]; then
+  make unittests
+  RETURN="$?"
+else
+  # The unittests makefile doesn't seem to have been packaged so get it from SVN
+  sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/
+  svn export  http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \
+      ../Makefile.unittest
+  sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/
+
+  make unittests \
+      DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
+      ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
+      ENABLE_SHARED=0
+  RETURN="$?"
+fi
 
 ###############################################################################
 # lit tests
 ###############################################################################
-# Note can't use ``make check`` because llvm-lit is not available
-cd test
-# The build system needs to generate this file before we can run lit
-make lit.site.cfg \
-    DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-    ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-    ENABLE_SHARED=0
-
-set +e # We want to let all the tests run before we exit
-lit -v .
-RETURN="${RETURN}$?"
+if [ "X${USE_CMAKE}" == "X1" ]; then
+  make integrationtests
+  RETURN="${RETURN}$?"
+else
+  # Note can't use ``make check`` because llvm-lit is not available
+  cd test
+  # The build system needs to generate this file before we can run lit
+  make lit.site.cfg \
+      DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
+      ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
+      ENABLE_SHARED=0
+
+  set +e # We want to let all the tests run before we exit
+  lit -v .
+  RETURN="${RETURN}$?"
+fi
 
 #generate and upload coverage if COVERAGE is set
 if [ ${COVERAGE} -eq 1 ]; then
diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh
index b2f608db..3d52457f 100755
--- a/.travis/testing-utils.sh
+++ b/.travis/testing-utils.sh
@@ -2,6 +2,14 @@
 # Make sure we exit if there is a failure
 set -e
 
+if [ "X${USE_CMAKE}" == "X1" ]; then
+    # The New CMake build system just needs the GTest sources regardless
+    # of LLVM version.
+    wget https://github.com/google/googletest/archive/release-1.7.0.zip
+    unzip release-1.7.0.zip
+    exit 0
+fi
+
 if [ "${LLVM_VERSION}" != "2.9" ]; then
     # Using LLVM3.4 all we need is vanilla GoogleTest :)
     wget https://github.com/google/googletest/archive/release-1.7.0.zip
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 00000000..bede4bc7
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,688 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+###############################################################################
+# Minimum CMake version and policies
+###############################################################################
+cmake_minimum_required(VERSION 2.8.12)
+if (POLICY CMP0054)
+  # FIXME: This is horrible. With the old behaviour,
+  # quoted strings like "MSVC" in if() conditionals
+  # get implicitly dereferenced. The NEW behaviour
+  # doesn't do this but CMP0054 was only introduced
+  # in CMake 3.1 and we support lower versions as the
+  # minimum. We could set NEW here but it would be very
+  # confusing to use NEW for some builds and OLD for others
+  # which could lead to some subtle bugs. Instead when the
+  # minimum version is 3.1 change this policy to NEW and remove
+  # the hacks in place to work around it.
+  cmake_policy(SET CMP0054 OLD)
+endif()
+
+if (POLICY CMP0042)
+  # Enable `MACOSX_RPATH` by default.
+  cmake_policy(SET CMP0042 NEW)
+endif()
+
+# This overrides the default flags for the different CMAKE_BUILD_TYPEs
+set(CMAKE_USER_MAKE_RULES_OVERRIDE_C
+  "${CMAKE_CURRENT_SOURCE_DIR}/cmake/c_flags_override.cmake")
+set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX
+  "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_flags_override.cmake")
+project(KLEE CXX C)
+
+###############################################################################
+# Project version
+###############################################################################
+set(KLEE_VERSION_MAJOR 1)
+set(KLEE_VERSION_MINOR 2)
+set(KLEE_VERSION_PATCH 0)
+set(KLEE_VERSION_TWEAK 0)
+set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}.${KLEE_VERSION_PATCH}.${KLEE_VERSION_TWEAK}")
+message(STATUS "KLEE version ${KLEE_VERSION}")
+set(PACKAGE_STRING "\"KLEE ${KLEE_VERSION}\"")
+set(PACKAGE_URL "\"https://klee.github.io\"")
+
+################################################################################
+# Set various useful variables depending on CMake version
+################################################################################
+if (("${CMAKE_VERSION}" VERSION_EQUAL "3.2") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.2"))
+  # In CMake >= 3.2 add_custom_command() supports a ``USES_TERMINAL`` argument
+  set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL")
+else()
+  set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "")
+endif()
+
+################################################################################
+# Sanity check - Disallow building in source.
+# Otherwise we would overwrite the Makefiles of the old build system.
+################################################################################
+if ("${CMAKE_SOURCE_DIR}" STREQUAL "${CMAKE_BINARY_DIR}")
+  message(FATAL_ERROR "In source builds are not allowed. You should invoke "
+          "CMake from a different directory.")
+endif()
+
+################################################################################
+# Build type
+################################################################################
+message(STATUS "CMake generator: ${CMAKE_GENERATOR}")
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi-configuration build (e.g. Xcode). Here
+  # CMAKE_BUILD_TYPE doesn't matter
+  message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}")
+else()
+  # Single configuration generator (e.g. Unix Makefiles, Ninja)
+  set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
+  if(NOT CMAKE_BUILD_TYPE)
+    message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default")
+    message(STATUS "The available build types are: ${available_build_types}")
+    set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE String
+        "Options are ${available_build_types}"
+        FORCE)
+    # Provide drop down menu options in cmake-gui
+    set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types})
+  endif()
+  message(STATUS "Build type: ${CMAKE_BUILD_TYPE}")
+
+  # Check the selected build type is valid
+  list(FIND available_build_types "${CMAKE_BUILD_TYPE}" _build_type_index)
+  if ("${_build_type_index}" EQUAL "-1")
+    message(FATAL_ERROR "\"${CMAKE_BUILD_TYPE}\" is an invalid build type.\n"
+      "Use one of the following build types ${available_build_types}")
+  endif()
+endif()
+
+
+################################################################################
+# Add our CMake module directory to the list of module search directories
+################################################################################
+list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules")
+
+################################################################################
+# Assertions
+################################################################################
+option(ENABLE_KLEE_ASSERTS "Enable KLEE assertions" ON)
+if (ENABLE_KLEE_ASSERTS)
+  message(STATUS "KLEE assertions enabled")
+  # Assume that -DNDEBUG isn't set.
+else()
+  message(STATUS "KLEE assertions disabled")
+  list(APPEND KLEE_COMPONENT_CXX_DEFINES "NDEBUG")
+endif()
+
+################################################################################
+# KLEE timestamps
+################################################################################
+option(KLEE_ENABLE_TIMESTAMP "Add timestamps to KLEE sources" OFF)
+
+################################################################################
+# Include useful CMake functions
+################################################################################
+include(GNUInstallDirs)
+include(CheckIncludeFile)
+include(CheckIncludeFileCXX)
+include(CheckFunctionExists)
+include(CheckPrototypeDefinition)
+include("${CMAKE_SOURCE_DIR}/cmake/string_to_list.cmake")
+include("${CMAKE_SOURCE_DIR}/cmake/klee_component_add_cxx_flag.cmake")
+include("${CMAKE_SOURCE_DIR}/cmake/add_global_flag.cmake")
+
+################################################################################
+# Compiler flags for KLEE components
+# Subsequent commands will append to these. These are used instead of
+# directly modifying CMAKE_CXX_FLAGS so that other code can be easily built with
+# different flags.
+################################################################################
+set(KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "")
+set(KLEE_COMPONENT_CXX_DEFINES "")
+set(KLEE_COMPONENT_CXX_FLAGS "")
+set(KLEE_SOLVER_LIBRARIES "")
+set(KLEE_COMPONENT_EXTRA_LIBRARIES "")
+
+################################################################################
+# Find LLVM
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/find_llvm.cmake)
+set(NEEDED_LLVM_VARS
+  LLVM_PACKAGE_VERSION
+  LLVM_VERSION_MAJOR
+  LLVM_VERSION_MINOR
+  LLVM_VERSION_PATCH
+  LLVM_DEFINITIONS
+  LLVM_ENABLE_ASSERTIONS
+  LLVM_ENABLE_EH
+  LLVM_ENABLE_RTTI
+  LLVM_INCLUDE_DIRS
+  LLVM_LIBRARY_DIRS
+  LLVM_TOOLS_BINARY_DIR
+  TARGET_TRIPLE
+)
+
+foreach (vname ${NEEDED_LLVM_VARS})
+  message(STATUS "${vname}: \"${${vname}}\"")
+  if (NOT (DEFINED "${vname}"))
+    message(FATAL_ERROR "${vname} was not defined")
+  endif()
+endforeach()
+
+if (LLVM_ENABLE_ASSERTIONS)
+  # Certain LLVM debugging macros only work when LLVM was built with asserts
+  set(ENABLE_KLEE_DEBUG 1) # for config.h
+else()
+  unset(ENABLE_KLEE_DEBUG) # for config.h
+endif()
+
+
+list(APPEND KLEE_COMPONENT_CXX_DEFINES ${LLVM_DEFINITIONS})
+list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${LLVM_INCLUDE_DIRS})
+
+# Find llvm-link
+set(LLVM_LINK "${LLVM_TOOLS_BINARY_DIR}/llvm-link")
+if (NOT EXISTS "${LLVM_LINK}")
+  message(FATAL_ERROR "Failed to find llvm-link at \"${LLVM_LINK}\"")
+endif()
+
+# Find llvm-ar
+set(LLVM_AR "${LLVM_TOOLS_BINARY_DIR}/llvm-ar")
+if (NOT EXISTS "${LLVM_AR}")
+  message(FATAL_ERROR "Failed to find llvm-ar at \"${LLVM_AR}\"")
+endif()
+
+# Find llvm-as
+set(LLVM_AS "${LLVM_TOOLS_BINARY_DIR}/llvm-as")
+if (NOT EXISTS "${LLVM_AS}")
+  message(FATAL_ERROR "Failed to find llvm-as at \"${LLVM_AS}\"")
+endif()
+
+################################################################################
+# Find bitcode compiler
+################################################################################
+include("${CMAKE_SOURCE_DIR}/cmake/find_bitcode_compiler.cmake")
+message(STATUS "LLVMCC: ${LLVMCC}")
+if (NOT EXISTS "${LLVMCC}")
+  message(FATAL_ERROR "Cannot find C bitcode compiler \"${LLVMCC}\"")
+endif()
+message(STATUS "LLVMCXX: ${LLVMCXX}")
+if (NOT EXISTS "${LLVMCXX}")
+  message(FATAL_ERROR "Cannot find C++ bitcode compiler \"${LLVMCXX}\"")
+endif()
+
+################################################################################
+# C++ version
+################################################################################
+option(USE_CXX11 "Use C++11" OFF)
+if ("${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.5.0")
+  message(STATUS "Using LLVM >= 3.5.0. Forcing using C++11")
+  set(USE_CXX11 ON CACHE BOOL "Use C++11" FORCE)
+endif()
+
+if (USE_CXX11)
+  message(STATUS "Enabling C++11")
+  # FIXME: Use CMake's own mechanism for managing C++ version.
+  # Set globally because it is unlikely we would want to compile
+  # using mixed C++ versions.
+  add_global_cxx_flag("-std=c++11" REQUIRED)
+else()
+  # This is needed because with GCC 6 the default changed from gnu++98 to
+  # gnu++14.
+  add_global_cxx_flag("-std=gnu++98" REQUIRED)
+endif()
+
+################################################################################
+# Warnings
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
+
+################################################################################
+# Solvers
+################################################################################
+
+# STP: Use CMake facility to detect. The user can pass `-DSTP_DIR=` to force
+# a particular directory.
+option(ENABLE_SOLVER_STP "Enable STP solver support" OFF)
+if (ENABLE_SOLVER_STP)
+  message(STATUS "STP solver support enabled")
+  # Although find_package() will set `STP_DIR` for us add it here so that
+  # is displayed in `ccmake` and `cmake-gui`.
+  set(STP_DIR "" CACHE PATH "Path to directory containing STPConfig.cmake")
+  find_package(STP CONFIG)
+  if (STP_FOUND)
+    message(STATUS "Found STP version ${STP_VERSION}")
+    # Try the STP shared library first
+    if ("${STP_SHARED_LIBRARY}" STREQUAL "")
+      # Try the static library instead
+      if ("${STP_STATIC_LIBRARY}" STREQUAL "")
+        message(FATAL_ERROR "Couldn't find STP shared or static library")
+      endif()
+      message(STATUS "Using STP static library")
+      list(APPEND KLEE_SOLVER_LIBRARIES "${STP_STATIC_LIBRARY}")
+    else()
+      message(STATUS "Using STP shared library")
+      list(APPEND KLEE_SOLVER_LIBRARIES "${STP_SHARED_LIBRARY}")
+    endif()
+    list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "${STP_INCLUDE_DIRS}")
+    message(STATUS "STP_DIR: ${STP_DIR}")
+    set(ENABLE_STP 1) # For config.h
+  else()
+    message(FATAL_ERROR "STP not found. Try setting `-DSTP_DIR=/path` where"
+      " `/path` is the directory containing `STPConfig.cmake`")
+  endif()
+else()
+  message(STATUS "STP solver support disabled")
+  set(ENABLE_STP 0) # For config.h
+endif()
+
+# Z3
+option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" OFF)
+if (ENABLE_SOLVER_Z3)
+  message(STATUS "Z3 solver support enabled")
+  find_package(Z3)
+  if (Z3_FOUND)
+    message(STATUS "Found Z3")
+    set(ENABLE_Z3 1) # For config.h
+    list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS})
+    list(APPEND KLEE_SOLVER_LIBRARIES ${Z3_LIBRARIES})
+
+    # Check the signature of `Z3_get_error_msg()`
+    set (_old_CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES}")
+    set(CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES} ${Z3_LIBRARIES})
+    check_prototype_definition(Z3_get_error_msg
+      "Z3_string Z3_get_error_msg(Z3_context c, Z3_error_code err)"
+      "NULL" "${Z3_INCLUDE_DIRS}/z3.h" HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT)
+    set(CMAKE_REQUIRED_LIBRARIES ${_old_CMAKE_REQUIRED_LIBRARIES})
+    if (HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT)
+      message(STATUS "Z3_get_error_msg requires context")
+    else()
+      message(STATUS "Z3_get_error_msg does not require context")
+    endif()
+  else()
+    message(FATAL_ERROR "Z3 not found.")
+  endif()
+else()
+  message(STATUS "Z3 solver support disabled")
+  set(ENABLE_Z3 0) # For config.h
+endif()
+
+# metaSMT
+option(ENABLE_SOLVER_METASMT "Enable metaSMT solver support" OFF)
+if (ENABLE_SOLVER_METASMT)
+  message(STATUS "metaSMT solver support enabled")
+  set(ENABLE_METASMT 1)
+  include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake)
+else()
+  message(STATUS "metaSMT solver support disabled")
+  set(ENABLE_METASMT 0) # For config.h
+endif()
+
+if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}))
+  message(FATAL_ERROR "No solver was specified. At least one solver is required."
+    "You should enable a solver by passing one of more the following options"
+    " to cmake:\n"
+    "\"-DENABLE_SOLVER_STP=ON\"\n"
+    "\"-DENABLE_SOLVER_Z3=ON\"\n"
+    "\"-DENABLE_SOLVER_METASMT=ON\"")
+endif()
+
+###############################################################################
+# Exception handling
+###############################################################################
+if (NOT LLVM_ENABLE_EH)
+  if (ENABLE_SOLVER_METASMT)
+    message(WARNING "Not disabling exceptions because metaSMT uses them")
+  else()
+    klee_component_add_cxx_flag("-fno-exceptions" REQUIRED)
+  endif()
+endif()
+
+###############################################################################
+# RTTI
+###############################################################################
+if (NOT LLVM_ENABLE_RTTI)
+  if (ENABLE_SOLVER_METASMT)
+    message(WARNING "Not disabling RTTI because metaSMT uses them")
+    # FIXME: Should this be FATAL_ERROR rather than ERROR?
+    message(WARNING
+      "This build configuration is not supported and will likely not work."
+      "You should recompile LLVM with RTTI enabled.")
+  else()
+    klee_component_add_cxx_flag("-fno-rtti" REQUIRED)
+  endif()
+endif()
+
+################################################################################
+# Support for compressed logs
+################################################################################
+find_package(ZLIB)
+if (${ZLIB_FOUND})
+  set(HAVE_ZLIB_H 1) # For config.h
+	set(TARGET_LIBS ${TARGET_LIBS} z)
+  list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${ZLIB_LIBRARIES})
+  list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${ZLIB_INCLUDE_DIRS})
+else()
+  unset(HAVE_ZLIB_H) # For config.h
+endif()
+
+################################################################################
+# TCMalloc support
+################################################################################
+OPTION(ENABLE_TCMALLOC "Enable TCMalloc support" OFF)
+if (ENABLE_TCMALLOC)
+  message(STATUS "TCMalloc support enabled")
+  set(TCMALLOC_HEADER "gperftools/malloc_extension.h")
+  check_include_file_cxx("${TCMALLOC_HEADER}" HAVE_GPERFTOOLS_MALLOC_EXTENSION_H)
+  if (${HAVE_GPERFTOOLS_MALLOC_EXTENSION_H})
+    find_library(TCMALLOC_LIBRARIES
+      NAMES tcmalloc tcmalloc_minimal
+      DOC "TCMalloc libraries"
+    )
+    if (NOT TCMALLOC_LIBRARIES)
+      message(FATAL_ERROR
+        "Found \"${TCMALLOC_HEADER}\" but could not find library")
+    endif()
+    list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${TCMALLOC_LIBRARIES})
+    if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+      # TCMalloc's documentation says its safest to pass these flags when
+      # building with gcc because gcc can optimize assuming its using its own
+      # malloc.
+      klee_component_add_cxx_flag(-fno-builtin-malloc REQUIRED)
+      klee_component_add_cxx_flag(-fno-builtin-calloc REQUIRED)
+      klee_component_add_cxx_flag(-fno-builtin-realloc REQUIRED)
+      klee_component_add_cxx_flag(-fno-builtin-free REQUIRED)
+    endif()
+  else()
+    message(FATAL_ERROR "Can't find \"${TCMALLOC_HEADER}\"")
+  endif()
+else()
+  message(STATUS "TCMalloc support disabled")
+endif()
+
+################################################################################
+# Detect libcap
+################################################################################
+check_include_file("sys/capability.h" HAVE_SYS_CAPABILITY_H)
+if (HAVE_SYS_CAPABILITY_H)
+  find_library(LIBCAP_LIBRARIES
+    NAMES cap
+    DOC "libcap library"
+  )
+  if (NOT LIBCAP_LIBRARIES)
+    message(FATAL_ERROR "Found \"sys/capability.h\" but could not find libcap")
+  endif()
+else()
+  set(LIBCAP_LIBRARIES "")
+endif()
+
+################################################################################
+# Detect libutil
+################################################################################
+check_include_file("pty.h" HAVE_PTY_H)
+if (HAVE_PTY_H)
+  find_library(LIBUTIL_LIBRARIES
+    NAMES util
+    DOC "libutil library. Typically part of glibc")
+  if (NOT LIBUTIL_LIBRARIES)
+    message(FATAL_ERROR "Found \"pty.h\" but could not find libutil")
+  endif()
+endif()
+
+################################################################################
+# Miscellaneous header file detection
+################################################################################
+check_function_exists(mallinfo HAVE_MALLINFO) # FIXME: should test CXX compiler not C
+check_function_exists(__ctype_b_loc HAVE_CTYPE_EXTERNALS) # FIXME: should test CXX compiler not C
+
+check_include_file_cxx(malloc/malloc.h HAVE_MALLOC_MALLOC_H)
+check_function_exists(malloc_zone_statistics HAVE_MALLOC_ZONE_STATISTICS)
+
+# FIXME: This is needed by the runtime not KLEE itself so we are testing the wrong
+# compiler.
+check_include_file("selinux/selinux.h" HAVE_SELINUX_SELINUX_H)
+check_include_file("sys/acl.h" HAVE_SYS_ACL_H)
+if (HAVE_SELINUX_SELINUX_H)
+  message(STATUS "SELinux support enabled")
+  set(HAVE_SELINUX 1)
+  # Test what function signature we need to use for SELinux. The signatures
+  # have changed between 2.2 and 2.3. In particular, the type of the "security
+  # context" parameter was changed from char * to const char *, with this
+  # patch: [PATCH] Get rid of security_context_t and fix const declarations.
+  # [http://www.spinics.net/lists/selinux/msg14827.html]
+  check_prototype_definition(setcon
+    "int setcon(char* context)"
+    "0"
+    "selinux/selinux.h"
+    SELINUX_SECURITY_CTX_NO_CONST
+  )
+  if (SELINUX_SECURITY_CTX_NO_CONST)
+    message(STATUS "security_context_t is char*")
+    set(KLEE_SELINUX_CTX_CONST " ")
+  else()
+    check_prototype_definition(setcon
+      "int setcon(const char* context)"
+      "0"
+      "selinux/selinux.h"
+      SELINUX_SECURITY_CTX_WITH_CONST
+    )
+    if (SELINUX_SECURITY_CTX_WITH_CONST)
+      message(STATUS "security_context_t is const char*")
+      set(KLEE_SELINUX_CTX_CONST "const")
+    else()
+      message(FATAL_ERROR "Failed to determine function signature for \"setcon\"")
+    endif()
+  endif()
+else()
+  message(STATUS "SELinux support disabled")
+  set(HAVE_SELINUX 0)
+endif()
+
+################################################################################
+# KLEE runtime support
+################################################################################
+# This is set here and not in `runtime` because `config.h` needs to be generated.
+
+
+set(available_klee_runtime_build_types
+  "Release"
+  "Release+Debug"
+  "Release+Asserts"
+  "Release+Debug+Asserts"
+  "Debug"
+  "Debug+Asserts"
+)
+if (NOT KLEE_RUNTIME_BUILD_TYPE)
+  message(STATUS "KLEE_RUNTIME_BUILD_TYPE is not set. Setting default")
+  message(STATUS "The available runtime build types are: ${available_klee_runtime_build_types}")
+  set(KLEE_RUNTIME_BUILD_TYPE "Release+Debug+Asserts" CACHE String
+    "Options are ${available_klee_runtime_build_types}"
+    FORCE)
+endif()
+# Provide drop down menu options in cmake-gui
+set_property(CACHE
+  KLEE_RUNTIME_BUILD_TYPE
+  PROPERTY STRINGS ${available_klee_runtime_build_types})
+message(STATUS "KLEE_RUNTIME_BUILD_TYPE: ${KLEE_RUNTIME_BUILD_TYPE}")
+
+set(KLEE_INSTALL_RUNTIME_DIR "${CMAKE_INSTALL_FULL_LIBDIR}/klee/runtime")
+
+# Location where KLEE will look for the built runtimes by default.
+set(KLEE_RUNTIME_DIRECTORY "${CMAKE_BINARY_DIR}/${KLEE_RUNTIME_BUILD_TYPE}/lib")
+
+################################################################################
+# KLEE POSIX Runtime Support
+################################################################################
+option(ENABLE_POSIX_RUNTIME "Enable KLEE's POSIX runtime" OFF)
+if (ENABLE_POSIX_RUNTIME)
+  message(STATUS "POSIX runtime enabled")
+  if (NOT ENABLE_KLEE_UCLIBC)
+    message(WARNING "Enabling POSIX runtime without klee-uclibc support."
+      "The runtime might not work without it. Pass `-DENABLE_KLEE_UCLIBC=ON`"
+      " to enable klee-uclibc support.")
+  endif()
+else()
+  message(STATUS "POSIX runtime disabled")
+endif()
+
+################################################################################
+# KLEE uclibc support
+################################################################################
+option(ENABLE_KLEE_UCLIBC "Enable support for klee-uclibc" OFF)
+if (ENABLE_KLEE_UCLIBC)
+  message(STATUS "klee-uclibc support enabled")
+  set(SUPPORT_KLEE_UCLIBC 1) # For config.h
+  set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory")
+  if (NOT IS_DIRECTORY "${KLEE_UCLIBC_PATH}")
+    message(FATAL_ERROR
+      "KLEE_UCLIBC_PATH (\"${KLEE_UCLIBC_PATH}\") is not a valid directory.\n"
+      "Try passing -DKLEE_UCLIBC_PATH=<path> to cmake where <path> is the path"
+      " to the root of the klee-uclibc directory.")
+  endif()
+
+  # Find the C library bitcode archive
+  set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca")
+  set(KLEE_UCLIBC_C_BCA "${KLEE_UCLIBC_PATH}/lib/libc.a")
+  if (NOT EXISTS "${KLEE_UCLIBC_PATH}")
+    message(FATAL_ERROR
+      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_BCA}\"")
+  endif()
+  message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_BCA}\"")
+  
+  # Make a symlink to KLEE_UCLIBC_C_BCA so KLEE can find it where it
+  # is expected.
+  file(MAKE_DIRECTORY "${KLEE_RUNTIME_DIRECTORY}")
+  execute_process(COMMAND ${CMAKE_COMMAND} -E create_symlink
+    "${KLEE_UCLIBC_C_BCA}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_NAME}"
+  )
+list(APPEND KLEE_COMPONENT_CXX_DEFINES
+  -DKLEE_UCLIBC_BCA_NAME=\"${KLEE_UCLIBC_BCA_NAME}\")
+
+# Add klee-uclibc to the install target. We install the original
+# file rather than the symlink because CMake would just copy the symlink
+# rather than the file.
+install(FILES "${KLEE_UCLIBC_C_BCA}"
+  DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}"
+  RENAME "${KLEE_UCLIBC_BCA_NAME}"
+  )
+
+else()
+  message(STATUS "klee-uclibc support disabled")
+  set(SUPPORT_KLEE_UCLIBC 0) # For config.h
+endif()
+
+################################################################################
+# Generate `config.h`
+################################################################################
+configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/config.h.cmin
+  ${CMAKE_BINARY_DIR}/include/klee/Config/config.h)
+
+################################################################################
+# Generate `CompileTimeInfo.h`
+################################################################################
+# FIXME: Get information from git and have configure depend on this so we
+# only re-generate the file when necessary.
+set(AUTO_GEN_MSG "AUTOMATICALLY GENERATED. DO NOT EDIT!")
+configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
+  ${CMAKE_BINARY_DIR}/include/klee/Config/CompileTimeInfo.h
+)
+
+################################################################################
+# Global include directories
+################################################################################
+include_directories("${CMAKE_SOURCE_DIR}/include")
+include_directories("${CMAKE_BINARY_DIR}/include")
+
+################################################################################
+# Set default location for targets in the build directory
+################################################################################
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+################################################################################
+# KLEE components
+################################################################################
+include("${CMAKE_SOURCE_DIR}/cmake/klee_add_component.cmake")
+add_subdirectory(lib)
+add_subdirectory(runtime)
+
+################################################################################
+# KLEE tools
+################################################################################
+add_subdirectory(tools)
+
+################################################################################
+# Testing
+################################################################################
+option(ENABLE_TESTS "Enable tests" ON)
+
+if (ENABLE_TESTS)
+  # Find lit
+  set(LIT_TOOL_NAMES "llvm-lit" "lit")
+  find_program(
+    LIT_TOOL
+    NAMES ${LIT_TOOL_NAMES}
+    HINTS "${LLVM_TOOLS_BINARY_DIR}"
+    DOC "Path to lit tool"
+  )
+
+  set(LIT_ARGS
+    "-v;-s"
+    CACHE
+    STRING
+    "Lit arguments"
+  )
+
+if ((NOT LIT_TOOL) OR (NOT EXISTS "${LIT_TOOL}"))
+    message(FATAL_ERROR "The lit tool is required for testing."
+      " CMake tried to find lit with the following names \"${LIT_TOOL_NAMES}\""
+      " but it could not be found.\n"
+      "You should either disable testing by passing \"-DENABLE_TESTS=OFF\" to cmake"
+      " or you should install the lit tool from the Python Package Index by running"
+      " \"pip install lit\". Note \"pip\" requires root privileges to run. If you"
+      " don't have root privileges you can create a virtual python environment using"
+      " the \"virtualenv\" tool and run \"pip\" from there.")
+  else()
+    message(STATUS "Using lit: ${LIT_TOOL}")
+  endif()
+
+  option(ENABLE_UNIT_TESTS "Enable unittests" ON)
+  if (ENABLE_UNIT_TESTS)
+    message(STATUS "Unit tests enabled")
+    add_subdirectory(unittests)
+  else()
+    message(STATUS "Unit tests disabled")
+  endif()
+  option(ENABLE_INTEGRATION_TESTS "Enable integration tests" ON)
+  if (ENABLE_INTEGRATION_TESTS)
+    message(STATUS "Integration tests enabled")
+    add_subdirectory(test)
+  else()
+    message(STATUS "Integration tests disabled")
+  endif()
+
+  # Add global test target
+  add_custom_target(check
+    DEPENDS unittests integrationtests
+    COMMENT "Running tests"
+  )
+else()
+  message(STATUS "Testing disabled")
+endif()
+
+################################################################################
+# Documentation
+################################################################################
+option(ENABLE_DOCS "Enable building documentation" ON)
+if (ENABLE_DOCS)
+  add_subdirectory(docs)
+endif()
+
+################################################################################
+# Miscellaneous install
+################################################################################
+install(FILES include/klee/klee.h DESTINATION include/klee)
diff --git a/Dockerfile b/Dockerfile
index 6ee9a9ac..f1cce2ee 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -13,7 +13,8 @@ ENV LLVM_VERSION=3.4 \
     KLEE_UCLIBC=klee_uclibc_v1.0.0 \
     KLEE_SRC=/home/klee/klee_src \
     COVERAGE=0 \
-    BUILD_DIR=/home/klee/klee_build
+    BUILD_DIR=/home/klee/klee_build \
+    USE_CMAKE=1
 
 RUN apt-get update && \
     apt-get -y --no-install-recommends install \
@@ -57,25 +58,7 @@ WORKDIR /home/klee
 
 # Copy across source files needed for build
 RUN mkdir ${KLEE_SRC}
-ADD configure \
-    LICENSE.TXT \
-    Makefile \
-    Makefile.* \
-    README.md \
-    MetaSMT.mk \
-    TODO.txt \
-    ${KLEE_SRC}/
-ADD .travis ${KLEE_SRC}/.travis/
-ADD autoconf ${KLEE_SRC}/autoconf/
-ADD docs ${KLEE_SRC}/docs/
-ADD include ${KLEE_SRC}/include/
-ADD lib ${KLEE_SRC}/lib/
-ADD runtime ${KLEE_SRC}/runtime/
-ADD scripts ${KLEE_SRC}/scripts/
-ADD test ${KLEE_SRC}/test/
-ADD tools ${KLEE_SRC}/tools/
-ADD unittests ${KLEE_SRC}/unittests/
-ADD utils ${KLEE_SRC}/utils/
+ADD / ${KLEE_SRC}
 
 # Set klee user to be owner
 RUN sudo chown --recursive klee: ${KLEE_SRC}
@@ -87,9 +70,12 @@ RUN mkdir -p ${BUILD_DIR}
 RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.sh
 
 # Install testing utils (use TravisCI script)
-RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \
+RUN cd ${BUILD_DIR} && mkdir test-utils && cd test-utils && \
     ${KLEE_SRC}/.travis/testing-utils.sh
 
+# FIXME: All these hacks need to be removed. Once we no longer
+# need to support KLEE's old build system they can be removed.
+
 # FIXME: This is a nasty hack so KLEE's configure and build finds
 # LLVM's headers file, libraries and tools
 RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \
@@ -108,13 +94,13 @@ RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \
 # FIXME: This is **really gross**. The Official Ubuntu LLVM packages don't ship
 # with ``FileCheck`` or the ``not`` tools so we have to hack building these
 # into KLEE's build system in order for the tests to pass
-RUN cd ${KLEE_SRC}/tools && \
+RUN [ "X${USE_CMAKE}" != "X1" ] && ( cd ${KLEE_SRC}/tools && \
     for tool in FileCheck not; do \
         svn export \
         http://llvm.org/svn/llvm-project/llvm/branches/release_34/utils/${tool} ${tool} ; \
         sed -i 's/^USEDLIBS.*$/LINK_COMPONENTS = support/' ${tool}/Makefile; \
     done && \
-    sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile
+    sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile ) || echo "Skipping hack"
 
 # FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist
 RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \
@@ -131,12 +117,16 @@ RUN mv /etc/sudoers.bak /etc/sudoers && \
 USER klee
 
 # Add KLEE binary directory to PATH
-RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc
+RUN [ "X${USE_CMAKE}" != "X1" ] && \
+  (echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc) || \
+  (echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/bin' >> /home/klee/.bashrc)
 
 # Link klee to /usr/bin so that it can be used by docker run
 USER root
-RUN for exec in ${BUILD_DIR}/klee/Release+Asserts/bin/* ; do ln -s ${exec} /usr/bin/`basename ${exec}`; done
+RUN [ "X${USE_CMAKE}" != "X1" ] && \
+  (for executable in ${BUILD_DIR}/klee/Release+Asserts/bin/* ; do ln -s ${executable} /usr/bin/`basename ${executable}`; done) || \
+  (for executable in ${BUILD_DIR}/klee/bin/* ; do ln -s ${executable} /usr/bin/`basename ${executable}`; done)
 
 # Link klee to the libkleeRuntest library needed by docker run
-RUN ln -s ${BUILD_DIR}/klee/Release+Asserts/lib/libkleeRuntest.so /usr/lib/libkleeRuntest.so.1.0
+RUN [ "X${USE_CMAKE}" != "X1" ] && (ln -s ${BUILD_DIR}/klee/Release+Asserts/lib/libkleeRuntest.so /usr/lib/libkleeRuntest.so.1.0) || echo "Skipping hack"
 USER klee
diff --git a/README-CMake.md b/README-CMake.md
new file mode 100644
index 00000000..0b9cfd61
--- /dev/null
+++ b/README-CMake.md
@@ -0,0 +1,83 @@
+# CMake build system
+
+KLEE now has a CMake build system which is intended to replace
+its autoconf/Makefile based build system.
+
+## Useful top level targets
+
+* `check` - Build and run all tests.
+* `clean` - Clean the build tree. Note this won't clean the runtime build.
+* `docs` - Build documentation
+* `edit_cache` - Show cmake/ccmake/cmake-gui interface for chaning configure options.
+* `help` - Show list of top level targets
+* `integrationtests` - Run integration tests
+* `unittests` - Build and run unittests
+
+## Useful CMake variables
+
+These can be set by passing `-DVAR_NAME=VALUE` to the CMake invocation.
+
+e.g.
+
+```
+cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src
+```
+* `LLVMCC` (STRING) - Path to the LLVM C compiler (e.g. Clang).
+
+* `LLVMCXX` (STRING) - Path to the LLVM C++ compiler (e.g. Clang++).
+
+* `CMAKE_BUILD_TYPE` (STRING) - Build type for KLEE. Can be
+  `Debug`, `Release`, `RelWithDebInfo` or `MinSizeRel`.
+
+* `DOWNLOAD_LLVM_TESTING_TOOLS` (BOOLEAN) - Force downloading
+   of LLVM testing tool sources.
+
+* `ENABLE_DOCS` (BOOLEAN) - Enable building documentation.
+
+* `ENABLE_DOXYGEN` (BOOLEAN) - Enable building doxygen documentation.
+
+* `ENABLE_INTEGRATION_TESTS` (BOOLEAN) - Enable KLEE integration tests.
+
+* `ENABLE_KLEE_ASSERTS` (BOOLEAN) - Enable assertions when building KLEE.
+
+* `ENABLE_KLEE_UCLIBC` (BOOLEAN) - Enable support for klee-uclibc.
+
+* `ENABLE_POSIX_RUNTIME` (BOOLEAN) - Enable POSIX runtime.
+
+* `ENABLE_SOLVER_METASMT` (BOOLEAN) - Enable MetaSMT solver support.
+
+* `ENABLE_SOLVER_STP` (BOOLEAN) - Enable STP solver support.
+
+* `ENABLE_SOLVER_Z3` (BOOLEAN) - Enable Z3 solver support.
+
+* `ENABLE_TCMALLOC` (BOOLEAN) - Enable TCMalloc support.
+
+* `ENABLE_TESTS` (BOOLEAN) - Enable testing.
+
+* `ENABLE_UNIT_TESTS` (BOOLEAN) - Enable KLEE unit tests.
+
+* `GTEST_SRC_DIR` (STRING) - Path to GTest source tree.
+
+* `KLEE_ENABLE_TIMESTAMP` (BOOLEAN) - Enable timestamps in KLEE sources.
+
+* `KLEE_UCLIBC_PATH` (STRING) - Path to klee-uclibc root directory.
+
+* `KLEE_RUNTIME_BUILD_TYPE` (STRING) - Build type for KLEE's runtimes.
+   Can be `Release`, `Release+Asserts`, `Debug` or `Debug+Asserts`.
+
+* `LIT_TOOL` (STRING) - Path to lit testing tool.
+
+* `LIT_ARGS` (STRING) - Semi-colon separated list of lit options.
+
+* `LLVM_CONFIG_BINARY` (STRING) - Path to `llvm-config` binary. This is
+   only relevant if `USE_CMAKE_FIND_PACKAGE_LLVM` is `FALSE`. This is used
+   to detect the LLVM version and find libraries.
+
+* `MAKE_BINARY` (STRING) - Path to `make` binary used to build KLEE's runtime.
+
+* `USE_CMAKE_FIND_PACKAGE_LLVM` (BOOLEAN) - Use `find_package(LLVM CONFIG)`
+   to find LLVM.
+
+* `USE_CXX11` (BOOLEAN) - Use C++11.
+
+* `WARNINGS_AS_ERRORS` (BOOLEAN) - Treat warnings as errors when building KLEE.
diff --git a/cmake/add_global_flag.cmake b/cmake/add_global_flag.cmake
new file mode 100644
index 00000000..893e1200
--- /dev/null
+++ b/cmake/add_global_flag.cmake
@@ -0,0 +1,55 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+include(CheckCXXCompilerFlag)
+include(CheckCCompilerFlag)
+include(CMakeParseArguments)
+
+function(add_global_cxx_flag flag)
+  CMAKE_PARSE_ARGUMENTS(add_global_cxx_flag "REQUIRED" "" "" ${ARGN})
+  string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
+  string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  unset(HAS_${SANITIZED_FLAG_NAME})
+  CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}_CXX)
+  if (add_global_cxx_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}_CXX)
+    message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it")
+  endif()
+  if (HAS_${SANITIZED_FLAG_NAME}_CXX)
+    message(STATUS "C++ compiler supports ${flag}")
+    # NOTE: Have to be careful here as CMAKE_CXX_FLAGS is a string
+    # and not a list.
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}" PARENT_SCOPE)
+  else()
+    message(STATUS "C++ compiler does not support ${flag}")
+  endif()
+endfunction()
+
+function(add_global_c_flag flag)
+  CMAKE_PARSE_ARGUMENTS(add_global_c_flag "REQUIRED" "" "" ${ARGN})
+  string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
+  string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  unset(HAS_${SANITIZED_FLAG_NAME})
+  CHECK_C_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}_C)
+  if (add_global_c_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}_C)
+    message(FATAL_ERROR "The flag \"${flag}\" is required but your C compiler doesn't support it")
+  endif()
+  if (HAS_${SANITIZED_FLAG_NAME}_C)
+    message(STATUS "C compiler supports ${flag}")
+    # NOTE: Have to be careful here as CMAKE_C_FLAGS is a string
+    # and not a list.
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}" PARENT_SCOPE)
+  else()
+    message(STATUS "C compiler does not support ${flag}")
+  endif()
+endfunction()
diff --git a/cmake/c_flags_override.cmake b/cmake/c_flags_override.cmake
new file mode 100644
index 00000000..1064022c
--- /dev/null
+++ b/cmake/c_flags_override.cmake
@@ -0,0 +1,24 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+#
+# This file overrides the default compiler flags for CMake's built-in
+# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set
+# here.  The main purpose is to make sure ``-DNDEBUG`` is never set by default.
+#
+#===------------------------------------------------------------------------===#
+if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU"))
+  # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed
+  set(CMAKE_C_FLAGS_INIT "")
+  set(CMAKE_C_FLAGS_DEBUG_INIT "-O0 -g")
+  set(CMAKE_C_FLAGS_MINSIZEREL_INIT "-Os")
+  set(CMAKE_C_FLAGS_RELEASE_INIT "-O3")
+  set(CMAKE_C_FLAGS_RELWITHDEBINFO_INIT "-O2 -g")
+else()
+  message(FATAL_ERROR "Overrides not set for compiler ${CMAKE_C_COMPILER_ID}")
+endif()
diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
new file mode 100644
index 00000000..9e6e67ef
--- /dev/null
+++ b/cmake/compiler_warnings.cmake
@@ -0,0 +1,80 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+###############################################################################
+# Compiler warnings
+#
+# NOTE: All these variables should be lists of flags and NOT a single string.
+###############################################################################
+# FIXME: -Wunused-parameter fires a lot so for now suppress it.
+set(GCC_AND_CLANG_WARNINGS_CXX
+  "-Wall"
+  "-Wextra"
+  "-Wno-unused-parameter")
+set(GCC_AND_CLANG_WARNINGS_C
+  "-Wall"
+  "-Wextra"
+  "-Wno-unused-parameter")
+set(GCC_ONLY_WARNINGS_C "")
+set(GCC_ONLY_WARNINGS_CXX "")
+set(CLANG_ONLY_WARNINGS_C "")
+set(CLANG_ONLY_WARNINGS_CXX "")
+
+###############################################################################
+# Check which warning flags are supported and use them globally
+###############################################################################
+set(CXX_WARNING_FLAGS_TO_CHECK "")
+set(C_WARNING_FLAGS_TO_CHECK "")
+
+if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
+  list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_CXX})
+  list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS_CXX})
+elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+  list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_CXX})
+  list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS_CXX})
+else()
+  message(AUTHOR_WARNING "Unknown compiler")
+endif()
+
+if ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")
+  list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_C})
+  list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS_C})
+elseif ("${CMAKE_C_COMPILER_ID}" MATCHES "Clang")
+  list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_C})
+  list(APPEND C_WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS_C})
+else()
+  message(AUTHOR_WARNING "Unknown compiler")
+endif()
+
+# Loop through flags and use the ones which the compiler supports
+foreach (flag ${CXX_WARNING_FLAGS_TO_CHECK})
+  # Note `add_global_cxx_flag()` is used rather than
+  # `klee_component_add_cxx_flag()` because warning
+  # flags are typically useful for building everything.
+  add_global_cxx_flag("${flag}")
+endforeach()
+foreach (flag ${C_WARNING_FLAGS_TO_CHECK})
+  add_global_c_flag("${flag}")
+endforeach()
+
+###############################################################################
+# Warnings as errors
+###############################################################################
+option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF)
+if (WARNINGS_AS_ERRORS)
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+    add_global_cxx_flag("-Werror" REQUIRED)
+    add_global_c_flag("-Werror" REQUIRED)
+  else()
+    message(AUTHOR_WARNING "Unknown compiler")
+  endif()
+  message(STATUS "Treating compiler warnings as errors")
+else()
+  message(STATUS "Not treating compiler warnings as errors")
+endif()
diff --git a/cmake/cxx_flags_override.cmake b/cmake/cxx_flags_override.cmake
new file mode 100644
index 00000000..0e3946fe
--- /dev/null
+++ b/cmake/cxx_flags_override.cmake
@@ -0,0 +1,25 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+#
+# This file overrides the default compiler flags for CMake's built-in
+# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set
+# here.  The main purpose is to make sure ``-DNDEBUG`` is never set by default.
+#
+#===------------------------------------------------------------------------===#
+
+if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+  # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed
+  set(CMAKE_CXX_FLAGS_INIT "")
+  set(CMAKE_CXX_FLAGS_DEBUG_INIT "-O0 -g")
+  set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os")
+  set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3")
+  set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g")
+else()
+  message(FATAL_ERROR "Overrides not set for compiler ${CMAKE_CXX_COMPILER_ID}")
+endif()
diff --git a/cmake/find_bitcode_compiler.cmake b/cmake/find_bitcode_compiler.cmake
new file mode 100644
index 00000000..615931f3
--- /dev/null
+++ b/cmake/find_bitcode_compiler.cmake
@@ -0,0 +1,96 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+#
+# This file tries to find compilers to build LLVM bitcode.
+# It is implicitly dependent on `find_llvm.cmake` already being run in the
+# same scope.
+#
+#===------------------------------------------------------------------------===#
+
+message(STATUS "Looking for bitcode compilers")
+
+find_program(
+  LLVMCC
+  NAMES "clang-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang" "llvm-gcc"
+   # Give the LLVM tools directory higher priority than the system directory.
+  HINTS "${LLVM_TOOLS_BINARY_DIR}"
+)
+if (LLVMCC)
+  message(STATUS "Found ${LLVMCC}")
+else()
+  message(FATAL_ERROR "Failed to find C bitcode compiler")
+endif()
+
+find_program(
+  LLVMCXX
+  NAMES "clang++-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang++" "llvm-g++"
+   # Give the LLVM tools directory higher priority than the system directory.
+  HINTS "${LLVM_TOOLS_BINARY_DIR}"
+)
+if (LLVMCXX)
+  message(STATUS "Found ${LLVMCXX}")
+else()
+  message(FATAL_ERROR "Failed to find C++ bitcode compiler")
+endif()
+
+# Check `llvm-dis` is available
+set(LLVM_DIS_TOOL "${LLVM_TOOLS_BINARY_DIR}/llvm-dis")
+if (NOT EXISTS "${LLVM_DIS_TOOL}")
+  message(FATAL_ERROR
+    "The llvm-dis tool cannot be found at \"${LLVM_DIS_TOOL}\"")
+endif()
+
+# Test compiler
+function(test_bitcode_compiler COMPILER SRC_EXT)
+  message(STATUS "Testing bitcode compiler ${COMPILER}")
+  set(SRC_FILE "${CMAKE_BINARY_DIR}/test_bitcode_compiler.${SRC_EXT}")
+  file(WRITE "${SRC_FILE}" "int main(int argc, char** argv) { return 0;}")
+  set(BC_FILE "${SRC_FILE}.bc")
+  execute_process(
+    COMMAND
+      "${COMPILER}"
+      "-c"
+      "-emit-llvm"
+      "-o" "${BC_FILE}"
+      "${SRC_FILE}"
+    RESULT_VARIABLE COMPILE_INVOKE_EXIT_CODE
+  )
+  if ("${COMPILE_INVOKE_EXIT_CODE}" EQUAL 0)
+    message(STATUS "Compile success")
+  else()
+    message(FATAL_ERROR "Compilation failed")
+  endif()
+
+  message(STATUS "Checking compatibility with LLVM ${LLVM_PACKAGE_VERSION}")
+  # Check if the LLVM version we are using is compatible
+  # with this compiler by invoking the `llvm-dis` tool
+  # on the generated bitcode.
+  set(LL_FILE "${SRC_FILE}.ll")
+  execute_process(
+    COMMAND
+      "${LLVM_DIS_TOOL}"
+      "-o" "${LL_FILE}"
+      "${BC_FILE}"
+    RESULT_VARIABLE LLVM_DIS_INVOKE_EXIT_CODE
+  )
+  if ("${LLVM_DIS_INVOKE_EXIT_CODE}" EQUAL 0)
+    message(STATUS "\"${COMPILER}\" is compatible")
+  else()
+    message(FATAL_ERROR "\"${COMPILER}\" is not compatible with LLVM ${LLVM_PACKAGE_VERSION}")
+  endif()
+
+  # Remove temporary files. It's okay to not remove these on failure
+  # as they will be useful for developer debugging.
+  file(REMOVE "${SRC_FILE}")
+  file(REMOVE "${BC_FILE}")
+  file(REMOVE "${LL_FILE}")
+endfunction()
+
+test_bitcode_compiler("${LLVMCC}" "c")
+test_bitcode_compiler("${LLVMCXX}" "cxx")
diff --git a/cmake/find_llvm.cmake b/cmake/find_llvm.cmake
new file mode 100644
index 00000000..60d7b3e4
--- /dev/null
+++ b/cmake/find_llvm.cmake
@@ -0,0 +1,166 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+#
+# This file provides multiple methods to detect LLVM.
+#
+# * llvm-config executable. This method is portable across LLVM build systems
+# (i.e. works if LLVM was built with autoconf/Makefile or with CMake).
+#
+# * find_package(LLVM CONFIG). This method only works if LLVM was built with
+# CMake or with LLVM >= 3.5 when built with the autoconf/Makefile build system
+# This method relies on the `LLVMConfig.cmake` file generated to be generated
+# by LLVM's build system.
+#
+#===------------------------------------------------------------------------===#
+
+option(USE_CMAKE_FIND_PACKAGE_LLVM "Use find_package(LLVM CONFIG) to find LLVM" OFF)
+
+if (USE_CMAKE_FIND_PACKAGE_LLVM)
+  find_package(LLVM CONFIG REQUIRED)
+
+  # Provide function to map LLVM components to libraries.
+  function(klee_get_llvm_libs output_var)
+    if (${LLVM_PACKAGE_VERSION} VERSION_LESS "3.5")
+      llvm_map_components_to_libraries(${output_var} ${ARGN})
+    else()
+      llvm_map_components_to_libnames(${output_var} ${ARGN})
+    endif()
+    set(${output_var} ${${output_var}} PARENT_SCOPE)
+  endfunction()
+else()
+  # Use the llvm-config binary to get the information needed.
+  # Try to detect it in the user's environment. The user can
+  # force a particular binary by passing `-DLLVM_CONFIG_BINARY=/path/to/llvm-config`
+  # to CMake.
+  find_program(LLVM_CONFIG_BINARY
+    NAMES llvm-config)
+  message(STATUS "LLVM_CONFIG_BINARY: ${LLVM_CONFIG_BINARY}")
+
+  if (NOT LLVM_CONFIG_BINARY)
+    message(FATAL_ERROR
+      "Failed to find llvm-config.\n"
+      "Try passing -DLLVM_CONFIG_BINARY=/path/to/llvm-config to cmake")
+  endif()
+
+  function(_run_llvm_config output_var)
+    set(_command "${LLVM_CONFIG_BINARY}" ${ARGN})
+    execute_process(COMMAND ${_command}
+      RESULT_VARIABLE _exit_code
+      OUTPUT_VARIABLE ${output_var}
+      OUTPUT_STRIP_TRAILING_WHITESPACE
+      ERROR_STRIP_TRAILING_WHITESPACE
+    )
+    if (NOT ("${_exit_code}" EQUAL "0"))
+      message(FATAL_ERROR "Failed running ${_command}")
+    endif()
+    set(${output_var} ${${output_var}} PARENT_SCOPE)
+  endfunction()
+
+  # Get LLVM version
+  _run_llvm_config(LLVM_PACKAGE_VERSION "--version")
+  # Try x.y.z patern
+  set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)\\.([0-9]+)$")
+  if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}")
+    string(REGEX REPLACE
+      "${_llvm_version_regex}"
+      "\\1"
+      LLVM_VERSION_MAJOR
+      "${LLVM_PACKAGE_VERSION}")
+    string(REGEX REPLACE
+      "${_llvm_version_regex}"
+      "\\2"
+      LLVM_VERSION_MINOR
+      "${LLVM_PACKAGE_VERSION}")
+    string(REGEX REPLACE
+      "${_llvm_version_regex}"
+      "\\3"
+      LLVM_VERSION_PATCH
+      "${LLVM_PACKAGE_VERSION}")
+  else()
+    # try x.y pattern
+    set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)$")
+    if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}")
+      string(REGEX REPLACE
+        "${_llvm_version_regex}"
+        "\\1"
+        LLVM_VERSION_MAJOR
+        "${LLVM_PACKAGE_VERSION}")
+    string(REGEX REPLACE
+      "${_llvm_version_regex}"
+      "\\2"
+      LLVM_VERSION_MINOR
+      "${LLVM_PACKAGE_VERSION}")
+    set(LLVM_VERSION_PATCH 0)
+    else()
+      message(FATAL_ERROR
+        "Failed to parse LLVM version from \"${LLVM_PACKAGE_VERSION}\"")
+    endif()
+  endif()
+
+  set(LLVM_DEFINITIONS "")
+  _run_llvm_config(_llvm_cpp_flags "--cppflags")
+  string_to_list("${_llvm_cpp_flags}" _llvm_cpp_flags_list)
+  foreach (flag ${_llvm_cpp_flags_list})
+    # Filter out -I flags by only looking for -D flags.
+    if ("${flag}" MATCHES "^-D" AND NOT ("${flag}" STREQUAL "-D_DEBUG"))
+      list(APPEND LLVM_DEFINITIONS "${flag}")
+    endif()
+  endforeach()
+
+  set(LLVM_ENABLE_ASSERTIONS ON)
+  set(LLVM_ENABLE_EH ON)
+  set(LLVM_ENABLE_RTTI ON)
+  _run_llvm_config(_llvm_cxx_flags "--cxxflags")
+  string_to_list("${_llvm_cxx_flags}" _llvm_cxx_flags_list)
+  foreach (flag ${_llvm_cxx_flags_list})
+    if ("${flag}" STREQUAL "-DNDEBUG")
+      # Note we don't rely on `llvm-config --build-mode` because
+      # that seems broken when LLVM is built with CMake.
+      set(LLVM_ENABLE_ASSERTIONS OFF)
+    elseif ("${flag}" STREQUAL "-fno-exceptions")
+      set(LLVM_ENABLE_EH OFF)
+    elseif ("${flag}" STREQUAL "-fno-rtti")
+      set(LLVM_ENABLE_RTTI OFF)
+    endif()
+  endforeach()
+
+  set(LLVM_INCLUDE_DIRS "")
+  foreach (flag ${_llvm_cpp_flags_list})
+    # Filter out -D flags by only looking for -I flags.
+    if ("${flag}" MATCHES "^-I")
+      string(REGEX REPLACE "^-I(.+)$" "\\1" _include_dir "${flag}")
+      list(APPEND LLVM_INCLUDE_DIRS "${_include_dir}")
+    endif()
+  endforeach()
+
+  _run_llvm_config(LLVM_LIBRARY_DIRS "--libdir")
+  _run_llvm_config(LLVM_TOOLS_BINARY_DIR "--bindir")
+  _run_llvm_config(TARGET_TRIPLE "--host-target")
+
+  # Provide function to map LLVM components to libraries.
+  function(klee_get_llvm_libs OUTPUT_VAR)
+    _run_llvm_config(_llvm_libs "--libfiles" ${ARGN})
+    string_to_list("${_llvm_libs}" _llvm_libs_list)
+
+    # Now find the system libs that are needed.
+    # FIXME: This is a hack. We should really create imported
+    # targets for the LLVM libraries and have them depend
+    # on the necessary system libraries.
+    _run_llvm_config(_system_libs "--ldflags")
+    string_to_list("${_system_libs}" _system_libs_list)
+    set(_filtered_system_libs_list "")
+    foreach (l ${_system_libs_list})
+      # Filter out `-L<path>`.
+      if ("${l}" MATCHES "^-l")
+        list(APPEND _filtered_system_libs_list "${l}")
+      endif()
+    endforeach()
+    set(${OUTPUT_VAR} ${_llvm_libs_list} ${_system_libs} PARENT_SCOPE)
+  endfunction()
+endif()
diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake
new file mode 100644
index 00000000..a0a02cb9
--- /dev/null
+++ b/cmake/find_metasmt.cmake
@@ -0,0 +1,92 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+find_package(metaSMT CONFIG)
+if (NOT metaSMT_FOUND)
+  message(FATAL_ERROR "metaSMT not found. Try setting `-DmetaSMT_DIR=/path` where"
+    " `/path` is the directory containing `metaSMTConfig.cmake`")
+endif()
+message(STATUS "metaSMT_DIR: ${metaSMT_DIR}")
+list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS
+  "${metaSMT_INCLUDE_DIR}" ${metaSMT_INCLUDE_DIRS})
+# FIXME: We should test linking
+list(APPEND KLEE_SOLVER_LIBRARIES ${metaSMT_LIBRARIES})
+
+# THIS IS HORRIBLE. The ${metaSMT_CXXFLAGS} variable
+# is badly formed. It is a string but we can't just split
+# on spaces because its contents looks like this
+# "  -DmetaSMT_BOOLECTOR_1_API -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS".
+# So handle defines specially
+string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_broken_list)
+list(LENGTH _metaSMT_CXXFLAGS_broken_list _metaSMT_CXXFLAGS_broken_list_length)
+math(EXPR _metaSMT_CXXFLAGS_broken_list_last_index "${_metaSMT_CXXFLAGS_broken_list_length} -1")
+set(_metasmt_flags "")
+set(_metasmt_defines "")
+set(_index_to_skip "")
+foreach (index RANGE 0 ${_metaSMT_CXXFLAGS_broken_list_last_index})
+  list(FIND _index_to_skip "${index}" _should_skip)
+  if ("${_should_skip}" EQUAL "-1")
+    list(GET _metaSMT_CXXFLAGS_broken_list ${index} _current_flag)
+    if ("${_current_flag}" MATCHES "^-D")
+      # This is a define
+      if ("${_current_flag}" MATCHES "^-D$")
+        # This is a bad define. We have just `-D` and the next item
+        # is the actually definition.
+        if ("${index}" EQUAL "${_metaSMT_CXXFLAGS_broken_list_last_index}")
+          message(FATAL_ERROR "Stray -D flag!")
+        else()
+          # Get next value
+          math(EXPR _next_index "${index} + 1")
+          list(GET _metaSMT_CXXFLAGS_broken_list ${_next_index} _next_flag)
+          if ("${_next_flag}" STREQUAL "")
+            message(FATAL_ERROR "Next flag shouldn't be empty!")
+          endif()
+          list(APPEND _metasmt_defines "-D${_next_flag}")
+          list(APPEND _index_to_skip "${_next_index}")
+        endif()
+      else()
+        # This is well formed defined (e.g. `-DHELLO`)
+        list(APPEND _metasmt_defines "${_current_flag}")
+      endif()
+    else()
+      # Regular flag
+      list(APPEND _metasmt_flags "${_current_flag}")
+    endif()
+  endif()
+endforeach()
+
+message(STATUS "metaSMT defines: ${_metasmt_defines}")
+list(APPEND KLEE_COMPONENT_CXX_DEFINES ${_metasmt_defines})
+
+message(STATUS "metaSMT flags: ${_metasmt_flags}")
+foreach (f ${_metasmt_flags})
+  # Test the flag and fail if it can't be used
+  klee_component_add_cxx_flag(${f} REQUIRED)
+endforeach()
+
+set(available_metasmt_backends "BTOR" "STP" "Z3")
+set(METASMT_DEFAULT_BACKEND "STP"
+  CACHE
+  STRING
+  "Default metaSMT backend. Availabe options ${available_metasmt_backends}")
+# Provide drop down menu options in cmake-gui
+set_property(CACHE METASMT_DEFAULT_BACKEND
+  PROPERTY STRINGS ${available_metasmt_backends})
+
+# Check METASMT_DEFAULT_BACKEND has a valid value.
+list(FIND available_metasmt_backends "${METASMT_DEFAULT_BACKEND}" _meta_smt_backend_index)
+if ("${_meta_smt_backend_index}" EQUAL "-1")
+  message(FATAL_ERROR
+    "Invalid metaSMT default backend (\"${METASMT_DEFAULT_BACKEND}\").\n"
+    "Valid values are ${available_metasmt_backends}")
+endif()
+
+# Set appropriate define
+list(APPEND KLEE_COMPONENT_CXX_DEFINES
+  -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND})
diff --git a/cmake/klee_add_component.cmake b/cmake/klee_add_component.cmake
new file mode 100644
index 00000000..28e271c5
--- /dev/null
+++ b/cmake/klee_add_component.cmake
@@ -0,0 +1,25 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+function(klee_add_component target_name)
+  add_library(${target_name} ${ARGN})
+  # Use of `PUBLIC` means these will propagate to targets that use this component.
+  if (("${CMAKE_VERSION}" VERSION_EQUAL "3.3") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.3"))
+    # In newer CMakes we can make sure that the flags are only used when compiling C++
+    target_compile_options(${target_name} PUBLIC
+      $<$<COMPILE_LANGUAGE:CXX>:${KLEE_COMPONENT_CXX_FLAGS}>)
+  else()
+    # For older CMakes just live with the warnings we get for passing C++ only flags
+    # to the C compiler.
+    target_compile_options(${target_name} PUBLIC ${KLEE_COMPONENT_CXX_FLAGS})
+  endif()
+  target_include_directories(${target_name} PUBLIC ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS})
+  target_compile_definitions(${target_name} PUBLIC ${KLEE_COMPONENT_CXX_DEFINES})
+  target_link_libraries(${target_name} PUBLIC ${KLEE_COMPONENT_EXTRA_LIBRARIES})
+endfunction()
diff --git a/cmake/klee_component_add_cxx_flag.cmake b/cmake/klee_component_add_cxx_flag.cmake
new file mode 100644
index 00000000..c866f6da
--- /dev/null
+++ b/cmake/klee_component_add_cxx_flag.cmake
@@ -0,0 +1,31 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+include(CheckCXXCompilerFlag)
+include(CMakeParseArguments)
+
+function(klee_component_add_cxx_flag flag)
+  CMAKE_PARSE_ARGUMENTS(klee_component_add_cxx_flag "REQUIRED" "" "" ${ARGN})
+  string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
+  string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  unset(HAS_${SANITIZED_FLAG_NAME})
+  CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME})
+  if (klee_component_add_cxx_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME})
+    message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it")
+  endif()
+  if (HAS_${SANITIZED_FLAG_NAME})
+    message(STATUS "C++ compiler supports ${flag}")
+    list(APPEND KLEE_COMPONENT_CXX_FLAGS "${flag}")
+    set(KLEE_COMPONENT_CXX_FLAGS ${KLEE_COMPONENT_CXX_FLAGS} PARENT_SCOPE)
+  else()
+    message(STATUS "C++ compiler does not support ${flag}")
+  endif()
+endfunction()
diff --git a/cmake/modules/FindZ3.cmake b/cmake/modules/FindZ3.cmake
new file mode 100644
index 00000000..b5f90974
--- /dev/null
+++ b/cmake/modules/FindZ3.cmake
@@ -0,0 +1,35 @@
+# Tries to find an install of the Z3 library and header files
+#
+# Once done this will define
+#  Z3_FOUND - BOOL: System has the Z3 library installed
+#  Z3_INCLUDE_DIRS - LIST:The GMP include directories
+#  Z3_LIBRARIES - LIST:The libraries needed to use Z3
+include(FindPackageHandleStandardArgs)
+
+# Try to find libraries
+find_library(Z3_LIBRARIES
+  NAMES z3
+  DOC "Z3 libraries"
+)
+if (Z3_LIBRARIES)
+  message(STATUS "Found Z3 libraries: \"${Z3_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find Z3 libraries")
+endif()
+
+# Try to find headers
+find_path(Z3_INCLUDE_DIRS
+  NAMES z3.h
+  DOC "Z3 C header"
+)
+if (Z3_INCLUDE_DIRS)
+  message(STATUS "Found Z3 include path: \"${Z3_INCLUDE_DIRS}\"")
+else()
+  message(STATUS "Could not find Z3 include path")
+endif()
+
+# TODO: We should check we can link some simple code against libz3
+
+# Handle QUIET and REQUIRED and check the necessary variables were set and if so
+# set ``Z3_FOUND``
+find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_INCLUDE_DIRS Z3_LIBRARIES)
diff --git a/cmake/string_to_list.cmake b/cmake/string_to_list.cmake
new file mode 100644
index 00000000..65c04413
--- /dev/null
+++ b/cmake/string_to_list.cmake
@@ -0,0 +1,13 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+function(string_to_list s output_var)
+  string(REPLACE " " ";" _output "${s}")
+  set(${output_var} ${_output} PARENT_SCOPE)
+endfunction()
diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
new file mode 100644
index 00000000..386298ce
--- /dev/null
+++ b/docs/CMakeLists.txt
@@ -0,0 +1,38 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+# Top level target for building all documentation
+add_custom_target(docs)
+
+option(ENABLE_DOXYGEN "Enable building doxygen documentation" ON)
+if (ENABLE_DOXYGEN)
+  find_package(Doxygen)
+  if (DOXYGEN_FOUND)
+    message(STATUS "Doxygen found")
+    set(abs_top_srcdir "${CMAKE_SOURCE_DIR}")
+    set(abs_top_builddir "${CMAKE_BINARY_DIR}")
+
+    # Configure the Doxyfile
+    configure_file(doxygen.cfg.in doxygen.cfg @ONLY)
+
+    # Add rule to build doxygen documentation
+    add_custom_target(doc-doxygen
+      COMMAND "${DOXYGEN_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/doxygen.cfg"
+      COMMENT "Generating Doxygen documentation"
+      ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+    )
+    add_dependencies(docs doc-doxygen)
+  else()
+    message(WARNING "Doxygen not found. Can't build Doxygen documentation")
+    set(ENABLE_DOXYGEN OFF
+      CACHE
+      BOOL
+      "Enable building doxygen documentation" FORCE)
+  endif()
+endif()
diff --git a/include/klee/Config/CompileTimeInfo.h.cmin b/include/klee/Config/CompileTimeInfo.h.cmin
new file mode 100644
index 00000000..e07de010
--- /dev/null
+++ b/include/klee/Config/CompileTimeInfo.h.cmin
@@ -0,0 +1,19 @@
+//===-- CompileTimeInfo.h ---------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+// @AUTO_GEN_MSG@
+#ifndef KLEE_COMPILE_TIME_INFO_H
+#define KLEE_COMPILE_TIME_INFO_H
+
+#define KLEE_BUILD_MODE "@CMAKE_BUILD_TYPE@ (Asserts: @ENABLE_KLEE_ASSERTS@)"
+// TODO: Implement support for these
+// KLEE_BUILD_REVISION
+// KLEE_BUILD_TAG
+
+#endif
diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin
new file mode 100644
index 00000000..c2a30c16
--- /dev/null
+++ b/include/klee/Config/config.h.cmin
@@ -0,0 +1,95 @@
+#ifndef KLEE_CONFIG_CONFIG_H
+#define KLEE_CONFIG_CONFIG_H
+
+/* Enable KLEE DEBUG checks */
+#cmakedefine ENABLE_KLEE_DEBUG @ENABLE_KLEE_DEBUG@
+
+/* Enable metaSMT API */
+#cmakedefine ENABLE_METASMT @ENABLE_METASMT@
+
+/* Using STP Solver backend */
+#cmakedefine ENABLE_STP @ENABLE_STP@
+
+/* Using Z3 Solver backend */
+#cmakedefine ENABLE_Z3 @ENABLE_Z3@
+
+/* Does the platform use __ctype_b_loc, etc. */
+#cmakedefine HAVE_CTYPE_EXTERNALS @HAVE_CTYPE_EXTERNALS@
+
+/* Define to 1 if you have the <gperftools/malloc_extension.h> header file. */
+#cmakedefine HAVE_GPERFTOOLS_MALLOC_EXTENSION_H @HAVE_GPERFTOOLS_MALLOC_EXTENSION_H@
+
+/* Define if mallinfo() is available on this platform. */
+#cmakedefine HAVE_MALLINFO @HAVE_MALLINFO@
+
+/* Define to 1 if you have the <malloc/malloc.h> header file. */
+#cmakedefine HAVE_MALLOC_MALLOC_H @HAVE_MALLOC_MALLOC_H@
+
+/* Define to 1 if you have the `malloc_zone_statistics' function. */
+#cmakedefine HAVE_MALLOC_ZONE_STATISTICS @HAVE_MALLOC_ZONE_STATISTICS@
+
+/* Define to 1 if you have the <selinux/selinux.h> header file. */
+#cmakedefine HAVE_SELINUX_SELINUX_H @HAVE_SELINUX_SELINUX_H@
+
+/* Define to 1 if you have the <sys/acl.h> header file. */
+#cmakedefine HAVE_SYS_ACL_H @HAVE_SYS_ACL_H@
+
+/* Define to 1 if you have the <sys/capability.h> header file. */
+#cmakedefine HAVE_SYS_CAPABILITY_H @HAVE_SYS_CAPABILITY_H@
+
+/* Z3 needs a Z3_context passed to Z3_get_error_msg() */
+#cmakedefine HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT @HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT@
+
+/* Define to 1 if you have the <zlib.h> header file. */
+#cmakedefine HAVE_ZLIB_H @HAVE_ZLIB_H@
+
+/* Enable time stamping the sources */
+#cmakedefine KLEE_ENABLE_TIMESTAMP @KLEE_ENABLE_TIMESTAMP@
+
+/* Define to empty or 'const' depending on how SELinux qualifies its security
+   context parameters. */
+#cmakedefine KLEE_SELINUX_CTX_CONST @KLEE_SELINUX_CTX_CONST@
+
+/* LLVM major version number */
+#cmakedefine LLVM_VERSION_MAJOR @LLVM_VERSION_MAJOR@
+
+/* LLVM minor version number */
+#cmakedefine LLVM_VERSION_MINOR @LLVM_VERSION_MINOR@
+
+/* Define to the address where bug reports for this package should be sent. */
+#cmakedefine PACKAGE_BUGREPORT @PACKAGE_BUGREPORT@
+
+/* Define to the full name of this package. */
+#cmakedefine PACKAGE_NAME @PACKAGE_NAME@
+
+/* Define to the full name and version of this package. */
+#cmakedefine PACKAGE_STRING @PACKAGE_STRING@
+
+/* Define to the one symbol short name of this package. */
+#cmakedefine PACKAGE_TARNAME @PACKAGE_TARNAME@
+
+/* Define to the home page for this package. */
+#cmakedefine PACKAGE_URL @PACKAGE_URL@
+
+/* Define to the version of this package. */
+#cmakedefine PACKAGE_VERSION @PACKAGE_VERSION@
+
+/* klee-uclibc is supported */
+#cmakedefine SUPPORT_KLEE_UCLIBC @SUPPORT_KLEE_UCLIBC@
+
+/* Configuration type of KLEE's runtime libraries */
+#define RUNTIME_CONFIGURATION "@KLEE_RUNTIME_BUILD_TYPE@"
+
+/* FIXME: This is a stupid name. Also this is only used for figuring out where
+the runtime directory is in the build tree. Instead we should just define a
+macro for that. That would simplify the C++ code.  */
+/* Root of the KLEE binary build directory */
+#define KLEE_DIR "@CMAKE_BINARY_DIR@"
+
+/* Install directory for KLEE binaries */
+#define KLEE_INSTALL_BIN_DIR "@CMAKE_INSTALL_FULL_BINDIR@"
+
+/* Install directory for KLEE runtime */
+#define KLEE_INSTALL_RUNTIME_DIR "@KLEE_INSTALL_RUNTIME_DIR@"
+
+#endif
diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt
new file mode 100644
index 00000000..13f76d42
--- /dev/null
+++ b/lib/Basic/CMakeLists.txt
@@ -0,0 +1,14 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+klee_add_component(kleeBasic
+	CmdLineOptions.cpp
+	ConstructSolverChain.cpp
+	KTest.cpp
+	Statistics.cpp
+)
diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
new file mode 100644
index 00000000..8a074932
--- /dev/null
+++ b/lib/CMakeLists.txt
@@ -0,0 +1,14 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+add_subdirectory(Basic)
+add_subdirectory(Support)
+add_subdirectory(Expr)
+add_subdirectory(Solver)
+add_subdirectory(Module)
+add_subdirectory(Core)
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
new file mode 100644
index 00000000..05e2cffa
--- /dev/null
+++ b/lib/Core/CMakeLists.txt
@@ -0,0 +1,29 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+klee_add_component(kleeCore
+	AddressSpace.cpp
+	CallPathManager.cpp
+	Context.cpp
+	CoreStats.cpp
+	ExecutionState.cpp
+	Executor.cpp
+	ExecutorTimers.cpp
+	ExecutorUtil.cpp
+	ExternalDispatcher.cpp
+	ImpliedValue.cpp
+	Memory.cpp
+	MemoryManager.cpp
+	PTree.cpp
+	Searcher.cpp
+	SeedInfo.cpp
+	SpecialFunctionHandler.cpp
+	StatsTracker.cpp
+	TimingSolver.cpp
+	UserSearcher.cpp
+)
diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt
new file mode 100644
index 00000000..6ea77544
--- /dev/null
+++ b/lib/Expr/CMakeLists.txt
@@ -0,0 +1,23 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+klee_add_component(kleaverExpr
+	ArrayCache.cpp
+	Assigment.cpp
+	Constraints.cpp
+	ExprBuilder.cpp
+	Expr.cpp
+	ExprEvaluator.cpp
+	ExprPPrinter.cpp
+	ExprSMTLIBPrinter.cpp
+	ExprUtil.cpp
+	ExprVisitor.cpp
+	Lexer.cpp
+	Parser.cpp
+	Updates.cpp
+)
diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt
new file mode 100644
index 00000000..a952ed17
--- /dev/null
+++ b/lib/Module/CMakeLists.txt
@@ -0,0 +1,20 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+klee_add_component(kleeModule
+	Checks.cpp
+	InstructionInfoTable.cpp
+	IntrinsicCleaner.cpp
+	KInstruction.cpp
+	KModule.cpp
+	LowerSwitch.cpp
+	ModuleUtil.cpp
+	Optimize.cpp
+	PhiCleaner.cpp
+	RaiseAsm.cpp
+)
diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt
new file mode 100644
index 00000000..8add4ad6
--- /dev/null
+++ b/lib/Solver/CMakeLists.txt
@@ -0,0 +1,32 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+klee_add_component(kleaverSolver
+	CachingSolver.cpp
+	CexCachingSolver.cpp
+	ConstantDivision.cpp
+	CoreSolver.cpp
+	DummySolver.cpp
+	FastCexSolver.cpp
+	IncompleteSolver.cpp
+	IndependentSolver.cpp
+	MetaSMTSolver.cpp
+	PCLoggingSolver.cpp
+	QueryLoggingSolver.cpp
+	SMTLIBLoggingSolver.cpp
+	Solver.cpp
+	SolverImpl.cpp
+	SolverStats.cpp
+	STPBuilder.cpp
+	STPSolver.cpp
+	ValidatingSolver.cpp
+	Z3Builder.cpp
+	Z3Solver.cpp
+)
+
+target_link_libraries(kleaverSolver PRIVATE ${KLEE_SOLVER_LIBRARIES})
diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt
new file mode 100644
index 00000000..4bf7ea7d
--- /dev/null
+++ b/lib/Support/CMakeLists.txt
@@ -0,0 +1,20 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+klee_add_component(kleeSupport
+	CompressionStream.cpp
+	ErrorHandling.cpp
+	MemoryUsage.cpp
+	PrintVersion.cpp
+	RNG.cpp
+	Time.cpp
+	Timer.cpp
+	TreeStream.cpp
+)
+
+target_link_libraries(kleeSupport PRIVATE ${ZLIB_LIBRARIES})
diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
new file mode 100644
index 00000000..68eb9016
--- /dev/null
+++ b/runtime/CMakeLists.txt
@@ -0,0 +1,145 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+add_subdirectory(Runtest)
+
+if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Release")
+  set(RUNTIME_IS_RELEASE 1)
+else()
+  set(RUNTIME_IS_RELEASE 0)
+endif()
+
+if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Asserts")
+  set(RUNTIME_HAS_ASSERTIONS 1)
+else()
+  set(RUNTIME_HAS_ASSERTIONS 0)
+endif()
+
+if ("${KLEE_RUNTIME_BUILD_TYPE}" MATCHES "Debug")
+  set(RUNTIME_HAS_DEBUG_SYMBOLS 1)
+else()
+  set(RUNTIME_HAS_DEBUG_SYMBOLS 0)
+endif()
+
+
+# FIXME: This is a horrible hack that needs to die.
+# Things are very inconsistent. The runtime instrinsic
+# is sometimes a LLVM module or a bitcode archive.
+if ("${LLVM_PACKAGE_VERSION}" VERSION_EQUAL "3.3" OR
+    "${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.3")
+  set(USE_RUNTIME_BINARY_TYPE_HACK 1)
+else()
+  set(USE_RUNTIME_BINARY_TYPE_HACK 0)
+endif()
+
+if (ENABLE_POSIX_RUNTIME)
+  set(BUILD_POSIX_RUNTIME 1)
+else()
+  set(BUILD_POSIX_RUNTIME 0)
+endif()
+
+# Configure the bitcode build system
+configure_file("Makefile.cmake.bitcode.config.in"
+  "Makefile.cmake.bitcode.config"
+  @ONLY
+)
+
+# Copy over the makefiles to the build directory
+configure_file("Makefile.cmake.bitcode" "Makefile.cmake.bitcode" COPYONLY)
+configure_file("Makefile.cmake.bitcode.rules" "Makefile.cmake.bitcode.rules" COPYONLY)
+
+# Makefile for root runtime directory
+# Copy over makefiles for libraries
+set(BITCODE_LIBRARIES "Intrinsic" "klee-libc")
+if (ENABLE_POSIX_RUNTIME)
+  list(APPEND BITCODE_LIBRARIES "POSIX")
+endif()
+foreach (bl ${BITCODE_LIBRARIES})
+  configure_file("${bl}/Makefile.cmake.bitcode"
+    "${CMAKE_CURRENT_BINARY_DIR}/${bl}/Makefile.cmake.bitcode"
+    COPYONLY)
+endforeach()
+
+# Find GNU make
+find_program(MAKE_BINARY
+  NAMES make gmake
+)
+
+if (NOT MAKE_BINARY)
+  message(STATUS "Failed to find make binary")
+endif()
+
+# Find env
+find_program(ENV_BINARY
+  NAMES env
+)
+if (NOT ENV_BINARY)
+  message(FATAL_ERROR "Failed to find env binary")
+endif()
+
+# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject
+# that shipped with CMake >= 3.1. Should we just avoid using this option? We don't really
+# need it unless we are patching gsl itself and need to rebuild.
+if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1"))
+  option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON)
+  if (KLEE_RUNTIME_ALWAYS_REBUILD)
+    set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1)
+  else()
+    set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 0)
+  endif()
+else()
+  set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
+  message(WARNING "KLEE's runtime will not be automatically rebuilt.")
+endif()
+
+# Build the runtime as an external project.
+# We do this because CMake isn't really suitable
+# for building the runtime because it can't handle
+# the source file dependencies properly.
+include(ExternalProject)
+ExternalProject_Add(BuildKLEERuntimes
+  SOURCE_DIR "${CMAKE_CURRENT_BINARY_DIR}"
+  BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}"
+  CONFIGURE_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+  # `env` is used here to make sure `MAKEFLAGS` of KLEE's build
+  # is not propagated into the bitcode build system.
+  BUILD_COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all
+  ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
+  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+)
+
+# FIXME: Invoke `make clean` in the bitcode build system
+# when the `clean` target is invoked.
+
+###############################################################################
+# Runtime install
+###############################################################################
+set(RUNTIME_FILES_TO_INSTALL)
+
+# This is quite fragile and depends on knowledge in the bitcode
+# build system. Hopefully it won't change very often though.
+
+# FIXME: This hack needs to die!
+if (USE_RUNTIME_BINARY_TYPE_HACK)
+  list(APPEND RUNTIME_FILES_TO_INSTALL
+    "${KLEE_RUNTIME_DIRECTORY}/kleeRuntimeIntrinsic.bc"
+    "${KLEE_RUNTIME_DIRECTORY}/klee-libc.bc")
+else()
+  list(APPEND RUNTIME_FILES_TO_INSTALL
+    "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimeIntrinsic.bca"
+    "${KLEE_RUNTIME_DIRECTORY}/libklee-libc.bca")
+endif()
+
+if (ENABLE_POSIX_RUNTIME)
+  list(APPEND RUNTIME_FILES_TO_INSTALL
+    "${KLEE_RUNTIME_DIRECTORY}/libkleeRuntimePOSIX.bca")
+endif()
+
+install(FILES
+  ${RUNTIME_FILES_TO_INSTALL}
+  DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}")
diff --git a/runtime/Intrinsic/Makefile.cmake.bitcode b/runtime/Intrinsic/Makefile.cmake.bitcode
new file mode 100644
index 00000000..654ee020
--- /dev/null
+++ b/runtime/Intrinsic/Makefile.cmake.bitcode
@@ -0,0 +1,22 @@
+#===--------------------------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+LEVEL := ../
+
+include $(LEVEL)/Makefile.cmake.bitcode.config
+
+LLVMCC.Flags += -fno-builtin
+
+# FIXME: This is a horrible hack
+ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1)
+	MODULE_NAME=kleeRuntimeIntrinsic
+else
+	ARCHIVE_NAME=kleeRuntimeIntrinsic
+endif
+
+include $(LEVEL)/Makefile.cmake.bitcode.rules
diff --git a/runtime/Makefile.cmake.bitcode b/runtime/Makefile.cmake.bitcode
new file mode 100644
index 00000000..94f8a60d
--- /dev/null
+++ b/runtime/Makefile.cmake.bitcode
@@ -0,0 +1,18 @@
+#===--------------------------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+LEVEL := ./
+include $(LEVEL)/Makefile.cmake.bitcode.config
+
+DIRS += Intrinsic
+DIRS += klee-libc
+ifneq ($(ENABLE_POSIX_RUNTIME),0)
+	DIRS += POSIX
+endif
+
+include $(LEVEL)/Makefile.cmake.bitcode.rules
diff --git a/runtime/Makefile.cmake.bitcode.config.in b/runtime/Makefile.cmake.bitcode.config.in
new file mode 100644
index 00000000..9d31e907
--- /dev/null
+++ b/runtime/Makefile.cmake.bitcode.config.in
@@ -0,0 +1,51 @@
+#===--------------------------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+#
+# @AUTO_GEN_MSG@
+#
+#===------------------------------------------------------------------------===#
+LLVMCC := @LLVMCC@
+LLVM_LINK := @LLVM_LINK@
+LLVM_AR := @LLVM_AR@
+LLVM_VERSION_MAJOR := @LLVM_VERSION_MAJOR@
+LLVM_VERSION_MINOR := @LLVM_VERSION_MINOR@
+
+ROOT_SRC := @CMAKE_CURRENT_SOURCE_DIR@
+RUNTIME_CMAKE_BINARY_DIR := @CMAKE_CURRENT_BINARY_DIR@
+ROOT_OBJ := @CMAKE_CURRENT_BINARY_DIR@/runtime_build_@KLEE_RUNTIME_BUILD_TYPE@/
+
+# FIXME: For legacy reasons this is where the libraries need to end up
+ARCHIVE_DEST := @KLEE_RUNTIME_DIRECTORY@
+MODULE_DEST := $(ARCHIVE_DEST)
+
+# Build type
+IS_RELEASE := @RUNTIME_IS_RELEASE@
+ASSERTIONS_ENABLED := @RUNTIME_HAS_ASSERTIONS@
+DEBUG_SYMBOLS_ENABLED := @RUNTIME_HAS_DEBUG_SYMBOLS@
+RUNTIME_CONFIG_STRING := @KLEE_RUNTIME_BUILD_TYPE@
+
+# Optional features
+ENABLE_POSIX_RUNTIME := @BUILD_POSIX_RUNTIME@
+
+# FIXME: Get rid of this!
+USE_MODULE_INSTEAD_OF_BCA := @USE_RUNTIME_BINARY_TYPE_HACK@
+
+# Commands
+MKDIR := mkdir
+RM := rm
+
+# Compiler flags
+LLVMCC.Flags += \
+	-I@CMAKE_SOURCE_DIR@/include \
+	-I@CMAKE_BINARY_DIR@/include \
+	-emit-llvm \
+	-std=gnu89 \
+	-D_DEBUG -D_GNU_SOURCE -D__STDC_LIMIT_MACROS -D__STDC_CONSTANT_MACROS
+
+LLVMCC.Warnings += -Wall -Wwrite-strings
diff --git a/runtime/Makefile.cmake.bitcode.rules b/runtime/Makefile.cmake.bitcode.rules
new file mode 100644
index 00000000..85151e2f
--- /dev/null
+++ b/runtime/Makefile.cmake.bitcode.rules
@@ -0,0 +1,163 @@
+#===--------------------------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+# This files defines the rules used for the bitcode build system. They are
+# inspired by LLVM's old Makefile build system.
+#===------------------------------------------------------------------------===#
+.PHONY: all build_at_level clean debug_vars
+
+CURRENT_DIR:= $(shell pwd)
+
+# Sanity checks
+ifndef LEVEL
+  $(error LEVEL must be defined)
+endif
+
+ifndef LLVMCC
+  $(error Makefile.cmake.bitconfig.config must be included)
+endif
+
+# Any changes to the files listed here will trigger a rebuild of the sources
+ADDITIONAL_BUILD_DEPS := $(CURRENT_DIR)/Makefile.cmake.bitcode \
+                         $(RUNTIME_CMAKE_BINARY_DIR)/Makefile.cmake.bitcode.config \
+                         $(RUNTIME_CMAKE_BINARY_DIR)/Makefile.cmake.bitcode
+
+# Handle VERBOSE
+VERBOSE ?= 0
+ifneq ($(VERBOSE),0)
+  Verb :=
+else
+  Verb := @
+endif
+#
+# Handle build mode flags
+ifeq ($(IS_RELEASE),1)
+LLVMCC.Flags += -O2
+else
+LLVMCC.Flags += -O0
+endif
+
+# Handle assertion flags
+ifeq ($(ASSERTIONS_ENABLED),0)
+LLVMCC.Flags += -DNDEBUG
+endif
+
+# Handle debug symbol flags
+ifneq ($(DEBUG_SYMBOLS_ENABLED),0)
+LLVMCC.Flags += -g
+endif
+
+ifdef DIRS
+# all directory recursion target
+all::
+	$(Verb) for dir in $(DIRS); do \
+		($(MAKE) -C $$dir -f Makefile.cmake.bitcode) || exit 1; \
+	done
+
+clean::
+	$(Verb) for dir in $(DIRS); do \
+		($(MAKE) -C $$dir -f Makefile.cmake.bitcode $@) || exit 1; \
+	done
+else
+# Build sources
+
+all:: build_at_level
+
+# Compute the directory to find sources
+DIR_SUFFIX := $(subst $(RUNTIME_CMAKE_BINARY_DIR),,$(CURRENT_DIR))
+SRC_DIR := $(abspath $(ROOT_SRC)/$(DIR_SUFFIX))
+LOCAL_BUILD_DIR := $(abspath $(ROOT_OBJ)/$(DIR_SUFFIX))
+
+C_SRCS := $(shell echo $(SRC_DIR)/*.c)
+C_SRCS_NO_DIR := $(notdir $(C_SRCS))
+BC_FILES_NO_DIR := $(C_SRCS_NO_DIR:.c=.bc)
+BC_FILES := $(addprefix $(LOCAL_BUILD_DIR)/,$(BC_FILES_NO_DIR))
+
+# All bitcode files have these additional dependencies
+$(BC_FILES) : $(ADDITIONAL_BUILD_DEPS)
+
+# Include dependency information generated by previous
+# compiler invocations if they exist
+-include $(BC_FILES:.bc=.dep)
+
+# Pattern rule to build bitcode files
+$(LOCAL_BUILD_DIR)/%.bc : $(SRC_DIR)/%.c
+	@echo "LLVMCC ($(RUNTIME_CONFIG_STRING)) $<"
+	$(Verb) $(MKDIR) -p $(LOCAL_BUILD_DIR)
+	$(Verb) $(LLVMCC) $(LLVMCC.Flags) $(LLVMCC.Warnings) $< -c -o $@ -MP -MMD -MF $(LOCAL_BUILD_DIR)/$*.dep
+
+clean::
+	@echo "Removing bitcode files"
+	$(Verb) $(RM) -f $(BC_FILES)
+	@echo "Removing dependency files"
+	$(Verb) $(RM) -f $(BC_FILES:.bc=.dep)
+
+
+ifndef MODULE_NAME
+ifndef ARCHIVE_NAME
+$(error MODULE_NAME or ARCHIVE_NAME must be defined)
+endif
+endif
+
+ifdef MODULE_NAME
+MODULE_FILE := $(MODULE_DEST)/$(MODULE_NAME).bc
+build_at_level:: $(MODULE_FILE)
+
+# Rule for building LLVM bitcode module
+$(MODULE_FILE): $(BC_FILES)
+	$(Verb) $(MKDIR) -p $(MODULE_DEST)
+	@echo "Creating LLVM module $@"
+	$(Verb)$(LLVM_LINK) -o $@ $^
+
+clean::
+	@echo "Removing LLVM module $(MODULE_FILE)"
+	$(Verb) $(RM) -f $(MODULE_FILE)
+endif # MODULE_NAME
+
+ifdef ARCHIVE_NAME
+ARCHIVE_FILE := $(ARCHIVE_DEST)/lib$(ARCHIVE_NAME).bca
+
+build_at_level:: $(ARCHIVE_FILE)
+
+# Rule for building LLVM bitcode archive
+$(ARCHIVE_FILE): $(BC_FILES)
+	$(Verb) $(MKDIR) -p $(ARCHIVE_DEST)
+	@echo "Creating LLVM archive $@"
+	$(Verb) $(RM) -f $@
+	$(Verb)$(LLVM_AR) rcs $@ $^
+
+clean::
+	@echo "Removing LLVM bitcode archive $(ARCHIVE_FILE)"
+	$(Verb) $(RM) -f $(ARCHIVE_FILE)
+
+endif # ARCHIVE_NAME
+
+
+endif # end not ifdef DIRS
+
+debug_vars:
+	@echo "********************************************************************************"
+	@echo "Makefile variables for debugging"
+	@echo "********************************************************************************"
+	@echo "ARCHIVE_FILE := $(ARCHIVE_FILE)"
+	@echo "ASSERTIONS_ENABLED := $(ASSERTIONS_ENABLED)"
+	@echo "BC_FILES := $(BC_FILES)"
+	@echo "BUILD_ROOT := $(BUILD_ROOT)"
+	@echo "C_SRCS := $(C_SRCS)"
+	@echo "CURRENT_DIR := $(CURRENT_DIR)"
+	@echo "DEBUG_SYMBOLS_ENABLED := $(DEBUG_SYMBOLS_ENABLED)"
+	@echo "IS_RELEASE := $(IS_RELEASE)"
+	@echo "LOCAL_BUILD_DIR := $(LOCAL_BUILD_DIR)"
+	@echo "LLVMCC := $(LLVMCC)"
+	@echo "LLVMCC.Flag := $(LLVMCC.Flags)"
+	@echo "LLVMCC.Warnings := $(LLVMCC.Warnings)"
+	@echo "MODULE_FILE := $(MODULE_FILE)"
+	@echo "ROOT_OBJ := $(ROOT_OBJ)"
+	@echo "RUNTIME_CONFIG_STRING := $(RUNTIME_CONFIG_STRING)"
+	@echo "SRC_DIR := $(SRC_DIR)"
+	@echo "VERBOSE := $(VERBOSE)"
diff --git a/runtime/POSIX/Makefile.cmake.bitcode b/runtime/POSIX/Makefile.cmake.bitcode
new file mode 100644
index 00000000..66e250ff
--- /dev/null
+++ b/runtime/POSIX/Makefile.cmake.bitcode
@@ -0,0 +1,15 @@
+#===--------------------------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+LEVEL := ../
+
+include $(LEVEL)/Makefile.cmake.bitcode.config
+
+ARCHIVE_NAME=kleeRuntimePOSIX
+
+include $(LEVEL)/Makefile.cmake.bitcode.rules
diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt
new file mode 100644
index 00000000..dd455861
--- /dev/null
+++ b/runtime/Runtest/CMakeLists.txt
@@ -0,0 +1,22 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+add_library(kleeRuntest SHARED
+  intrinsics.c
+  # HACK:
+  ${CMAKE_SOURCE_DIR}/lib/Basic/KTest.cpp
+)
+# Increment version appropriately if ABI/API changes, more details:
+# http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html#AEN135
+set(KLEE_RUNTEST_VERSION 1.0)
+set_target_properties(kleeRuntest
+  PROPERTIES
+    VERSION ${KLEE_RUNTEST_VERSION}
+    SOVERSION ${KLEE_RUNTEST_VERSION}
+)
diff --git a/runtime/klee-libc/Makefile.cmake.bitcode b/runtime/klee-libc/Makefile.cmake.bitcode
new file mode 100644
index 00000000..6e85952c
--- /dev/null
+++ b/runtime/klee-libc/Makefile.cmake.bitcode
@@ -0,0 +1,24 @@
+#===--------------------------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+LEVEL := ../
+
+include $(LEVEL)/Makefile.cmake.bitcode.config
+
+# Prevent glibc from inlining some definitions
+# of builtins
+LLVMCC.Flags += -D__NO_INLINE__
+
+# FIXME: This is a horrible hack
+ifeq ($(USE_MODULE_INSTEAD_OF_BCA),1)
+	MODULE_NAME=klee-libc
+else
+	ARCHIVE_NAME=klee-libc
+endif
+
+include $(LEVEL)/Makefile.cmake.bitcode.rules
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
new file mode 100644
index 00000000..6d3ec926
--- /dev/null
+++ b/test/CMakeLists.txt
@@ -0,0 +1,139 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+set(KLEE_TOOLS_DIR "${CMAKE_BINARY_DIR}/bin")
+set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}")
+# FIXME: Do this to avoid changing the template file that
+# is shared by both build systems.
+set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include")
+set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include")
+set(TARGET_TRIPLE "${TARGET_TRIPLE}")
+if (ENABLE_KLEE_UCLIBC)
+  set(ENABLE_UCLIBC 1)
+else()
+  set(ENABLE_UCLIBC 0)
+endif()
+
+# FIXME: Do this to avoid changing the template file that
+# is shared by both build systems.
+if (ENABLE_POSIX_RUNTIME)
+  if (ENABLE_KLEE_UCLIBC)
+    set(ENABLE_POSIX_RUNTIME 1)
+  else()
+    message(AUTHOR_WARNING
+      "Disabling POSIX runtime tests because they depend on klee-uclibc"
+      "\nFIXME!")
+  set(ENABLE_POSIX_RUNTIME 0)
+  endif()
+else()
+  set(ENABLE_POSIX_RUNTIME 0)
+endif()
+
+###############################################################################
+# Find LLVM testing tools
+###############################################################################
+option(DOWNLOAD_LLVM_TESTING_TOOLS "Always download LLVM testing tools sources" OFF)
+mark_as_advanced(DOWNLOAD_LLVM_TESTING_TOOLS)
+
+# Check `FileCheck` and the `not` tools are available.  By default we'll try
+# looking in the LLVM binary directory.  If that fails download the sources.
+# This might be necessary if using a shipped version of LLVM because LLVM
+# unfortunately does not ship its testing tools.
+set(DOWNLOAD_FILECHECK_SOURCE FALSE)
+set(DOWNLOAD_NOT_SOURCE FALSE)
+
+if (DOWNLOAD_LLVM_TESTING_TOOLS)
+  set(DOWNLOAD_FILECHECK_SOURCE TRUE)
+  set(DOWNLOAD_NOT_SOURCE TRUE)
+endif()
+
+if (NOT EXISTS "${LLVM_TOOLS_BINARY_DIR}/FileCheck")
+  message(WARNING "\"${LLVM_TOOLS_BINARY_DIR}/FileCheck\" does not exist. Downloading sources.")
+  set(DOWNLOAD_FILECHECK_SOURCE TRUE)
+endif()
+
+if (NOT EXISTS "${LLVM_TOOLS_BINARY_DIR}/not")
+  message(WARNING "\"${LLVM_TOOLS_BINARY_DIR}/not\" does not exist. Downloading sources.")
+  set(DOWNLOAD_NOT_SOURCE TRUE)
+endif()
+
+if (DOWNLOAD_FILECHECK_SOURCE)
+  set(FILECHECK_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/utils/FileCheck/FileCheck.cpp")
+  set(FILECHECK_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/FileCheck.cpp")
+  if (NOT EXISTS "${FILECHECK_SRC_URL}")
+    message(STATUS "Downloading LLVM FileCheck source")
+    file(DOWNLOAD "${FILECHECK_SRC_URL}" "${FILECHECK_SRC_FILE}" SHOW_PROGRESS)
+  endif()
+  add_executable(FileCheck
+    ${FILECHECK_SRC_FILE}
+  )
+  klee_get_llvm_libs(FILECHECK_NEEDED_LIBS Support)
+  target_include_directories(FileCheck PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS})
+  target_compile_options(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
+  target_compile_definitions(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
+  target_link_libraries(FileCheck PRIVATE ${FILECHECK_NEEDED_LIBS})
+endif()
+
+if (DOWNLOAD_NOT_SOURCE)
+  set(NOT_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/utils/not/not.cpp")
+  set(NOT_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/not.cpp")
+  if (NOT EXISTS "${NOT_SRC_FILE}")
+    message(STATUS "Downloading LLVM not source")
+    file(DOWNLOAD "${NOT_SRC_URL}" "${NOT_SRC_FILE}" SHOW_PROGRESS)
+  endif()
+  add_executable("not"
+    ${NOT_SRC_FILE}
+  )
+  klee_get_llvm_libs(NOT_NEEDED_LIBS Support)
+  target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS})
+  target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
+  target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
+  target_link_libraries("not" PRIVATE ${FILECHECK_NEEDED_LIBS})
+endif()
+
+###############################################################################
+# Concrete tests build system
+###############################################################################
+add_subdirectory(Concrete)
+
+###############################################################################
+# Configure lit test suite
+###############################################################################
+configure_file(lit.site.cfg.in
+  ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg
+  @ONLY
+)
+
+add_custom_target(integrationtests
+  COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS klee kleaver
+  COMMENT "Running integration tests"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+# Tell CMake to remove lit's output directories when
+# running `make clean`.
+file(GLOB_RECURSE
+  test_contents
+  LIST_DIRECTORIES true
+  RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}"
+  "*"
+)
+set(dirs_to_clean "")
+foreach (f ${test_contents})
+  if (IS_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/${f}")
+    list(APPEND dirs_to_clean "${CMAKE_CURRENT_BINARY_DIR}/${f}/Output")
+  endif()
+endforeach()
+set_property(
+  DIRECTORY
+  APPEND
+  PROPERTY ADDITIONAL_MAKE_CLEAN_FILES
+  ${dirs_to_clean}
+)
diff --git a/test/Concrete/CMakeLists.txt b/test/Concrete/CMakeLists.txt
new file mode 100644
index 00000000..b3e4948f
--- /dev/null
+++ b/test/Concrete/CMakeLists.txt
@@ -0,0 +1,9 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+configure_file(Makefile.cmake.test.in Makefile.cmake.test @ONLY)
diff --git a/test/Concrete/ConcreteTest.py b/test/Concrete/ConcreteTest.py
index 754c0fe6..66d18c83 100755
--- a/test/Concrete/ConcreteTest.py
+++ b/test/Concrete/ConcreteTest.py
@@ -8,11 +8,16 @@ import sys
 import shutil
 
 def testFile(name, klee_path, lli_path):
+    print("CWD: \"{}\"".format(os.getcwd()))
     baseName,ext = os.path.splitext(name)
     exeFile = 'Output/linked_%s.bc'%baseName
 
     print('-- building test bitcode --')
-    make_cmd = 'make %s 2>&1' % (exeFile,)
+    if os.path.exists("Makefile.cmake.test"):
+        # Prefer CMake generated make file
+        make_cmd = 'make -f Makefile.cmake.test %s 2>&1' % (exeFile,)
+    else:
+        make_cmd = 'make %s 2>&1' % (exeFile,)
     print("EXECUTING: %s" % (make_cmd,))
     sys.stdout.flush()
     if os.system(make_cmd):
diff --git a/test/Concrete/Makefile.cmake.test.in b/test/Concrete/Makefile.cmake.test.in
new file mode 100644
index 00000000..feb879de
--- /dev/null
+++ b/test/Concrete/Makefile.cmake.test.in
@@ -0,0 +1,48 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+#
+# @AUTO_GEN_MSG@
+#
+#===------------------------------------------------------------------------===#
+LLVMCC := @LLVMCC@
+LLVMAS := @LLVM_AS@
+LLVMLINK := @LLVM_LINK@
+LLVMCC.CFlags := -O0 -Wall
+
+# Make sure source files can match the pattern rules
+VPATH := @CMAKE_CURRENT_SOURCE_DIR@
+
+Output/.dir:
+	mkdir -p $@
+
+clean::
+	-rm -rf Output/
+
+Output/%.bc: %.c Output/.dir
+	$(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@
+
+Output/%.bc: %.ll $(LLVMAS) Output/.dir
+	$(LLVMAS) -f $< -o $@
+
+# We build a separate testingUtils bitcode for each test, to make sure parallel
+# tests don't interact with one another.
+Output/%_testingUtils.bc: _testingUtils.c Output/.dir
+	$(LLVMCC) -emit-llvm -c $(LLVMCC.CFlags) $< -o $@
+
+Output/linked_%.bc: Output/%.bc Output/%_testingUtils.bc
+	$(LLVMLINK) $< Output/$*_testingUtils.bc -o $@
+
+.PRECIOUS: Output/.dir
+
+## Cancel built-in implicit rules that override above rules
+%: %.s
+
+%: %.c
+
+%.o: %.c
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
new file mode 100644
index 00000000..9bf2acf8
--- /dev/null
+++ b/tools/CMakeLists.txt
@@ -0,0 +1,14 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+add_subdirectory(gen-random-bout)
+add_subdirectory(kleaver)
+add_subdirectory(klee)
+add_subdirectory(klee-replay)
+add_subdirectory(klee-stats)
+add_subdirectory(ktest-tool)
diff --git a/tools/gen-random-bout/CMakeLists.txt b/tools/gen-random-bout/CMakeLists.txt
new file mode 100644
index 00000000..d1fa6b09
--- /dev/null
+++ b/tools/gen-random-bout/CMakeLists.txt
@@ -0,0 +1,17 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+add_executable(gen-random-bout
+	gen-random-bout.cpp
+)
+
+set(KLEE_LIBS kleeBasic)
+
+target_link_libraries(gen-random-bout ${KLEE_LIBS})
+
+install(TARGETS gen-random-bout RUNTIME DESTINATION bin)
diff --git a/tools/kleaver/CMakeLists.txt b/tools/kleaver/CMakeLists.txt
new file mode 100644
index 00000000..befbcc6e
--- /dev/null
+++ b/tools/kleaver/CMakeLists.txt
@@ -0,0 +1,18 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+add_executable(kleaver
+	main.cpp
+)
+
+klee_get_llvm_libs(LLVM_LIBS support)
+set(KLEE_LIBS kleeBasic kleaverSolver kleaverExpr kleeSupport)
+
+target_link_libraries(kleaver ${KLEE_LIBS} ${LLVM_LIBS})
+
+install(TARGETS kleaver RUNTIME DESTINATION bin)
diff --git a/tools/klee-replay/CMakeLists.txt b/tools/klee-replay/CMakeLists.txt
new file mode 100644
index 00000000..e0eb8d07
--- /dev/null
+++ b/tools/klee-replay/CMakeLists.txt
@@ -0,0 +1,30 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+if (HAVE_PTY_H)
+  add_executable(klee-replay
+    fd_init.c
+    file-creator.c
+    klee-replay.c
+    klee_init_env.c
+  )
+
+  target_link_libraries(klee-replay PRIVATE kleeBasic ${LIBCAP_LIBRARIES})
+  # FIXME: This isn't quite right. This is actually an implementation detail
+  # of glibc not Linux. Really we need to test if we can use `openpty()`
+  # with/without an additional library.
+  if ("${CMAKE_SYSTEM_NAME}" MATCHES "Linux")
+    if (NOT LIBUTIL_LIBRARIES)
+      message(FATAL_ERROR "klee-replay needs libutil under Linux")
+    endif()
+    target_link_libraries(klee-replay PRIVATE ${LIBUTIL_LIBRARIES})
+  endif()
+install(TARGETS klee-replay RUNTIME DESTINATION bin)
+else()
+  message(WARNING "Not building klee-replay due to missing \"pty.h\" header file")
+endif()
diff --git a/tools/klee-stats/CMakeLists.txt b/tools/klee-stats/CMakeLists.txt
new file mode 100644
index 00000000..7203003d
--- /dev/null
+++ b/tools/klee-stats/CMakeLists.txt
@@ -0,0 +1,9 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+install(PROGRAMS klee-stats DESTINATION bin)
diff --git a/tools/klee/CMakeLists.txt b/tools/klee/CMakeLists.txt
new file mode 100644
index 00000000..b6e907ab
--- /dev/null
+++ b/tools/klee/CMakeLists.txt
@@ -0,0 +1,39 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+add_executable(klee
+	main.cpp
+)
+
+# FIXME: This shouldn't be done here. Instead the KLEE libraries
+# should declare their LLVM dependencies.
+set(LLVM_COMPONENTS
+	bitreader
+	bitwriter
+	engine
+	ipo
+	jit
+	linker
+	support
+)
+
+if ("${LLVM_PACKAGE_VERSION}" VERSION_EQUAL "3.3" OR
+    "${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.3")
+  list(APPEND LLVM_COMPONENTS irreader)
+endif()
+
+klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
+
+set(KLEE_LIBS kleeCore kleeBasic kleeModule kleaverSolver kleaverExpr kleeSupport)
+
+target_link_libraries(klee ${KLEE_LIBS} ${LLVM_LIBS})
+
+install(TARGETS klee RUNTIME DESTINATION bin)
+
+# The KLEE binary depends on the runtimes
+add_dependencies(klee BuildKLEERuntimes)
diff --git a/tools/ktest-tool/CMakeLists.txt b/tools/ktest-tool/CMakeLists.txt
new file mode 100644
index 00000000..76e31ac0
--- /dev/null
+++ b/tools/ktest-tool/CMakeLists.txt
@@ -0,0 +1,13 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+install(PROGRAMS ktest-tool DESTINATION bin)
+
+# Copy into the build directory's binary directory
+# so integration tests can find it
+configure_file(ktest-tool "${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/ktest-tool" COPYONLY)
diff --git a/unittests/Assignment/CMakeLists.txt b/unittests/Assignment/CMakeLists.txt
new file mode 100644
index 00000000..e231ee39
--- /dev/null
+++ b/unittests/Assignment/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_klee_unit_test(AssignmentTest
+  AssignmentTest.cpp)
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(AssignmentTest PRIVATE kleaverExpr ${LLVM_LIBS})
diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
new file mode 100644
index 00000000..a85c0a74
--- /dev/null
+++ b/unittests/CMakeLists.txt
@@ -0,0 +1,100 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+# Build GTest. We don't use a pre-built version due to
+# https://github.com/google/googletest/blob/master/googletest/docs/FAQ.md#why-is-it-not-recommended-to-install-a-pre-compiled-copy-of-google-test-for-example-into-usrlocal
+set(GTEST_SRC_DIR
+  "/usr/src/gtest"
+  CACHE
+  PATH
+  "Path to GTest source directory"
+)
+
+if (NOT EXISTS "${GTEST_SRC_DIR}")
+  message(FATAL_ERROR "GTest source directory \"${GTEST_SRC_DIR}\" cannot be found.\n"
+    "Try passing -DGTEST_SRC_DIR=<path_to_gtest_source> to cmake where "
+    "<path_to_gtest_source> is the path to the GoogleTest source tree.\n"
+    "Alternatively you can disable unit tests by passing "
+    "-DENABLE_UNIT_TESTS=OFF to cmake.")
+endif()
+
+# It's important that GTest is built with KLEE's compile flags
+# so set them here.
+set(_OLD_CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}")
+foreach (f ${KLEE_COMPONENT_CXX_FLAGS})
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${f}")
+endforeach()
+foreach (f ${KLEE_COMPONENT_CXX_DEFINES})
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${f}")
+endforeach()
+
+# Build GTest as part of our project
+# FIXME: Prevent GTest from adding to our install target.
+# This is a problem for GTest >= 1.8. I've filled a PR to fix the issue
+# ( https://github.com/google/googletest/pull/921 ). If it gets accepted
+# we can do `set(gtest_enable_install FALSE)` to fix this.
+add_subdirectory(${GTEST_SRC_DIR} "${CMAKE_CURRENT_BINARY_DIR}/gtest_build")
+
+set(CMAKE_CXX_FLAGS "${_OLD_CMAKE_CXX_FLAGS}") # Restore the flags
+
+# This keeps track of all the unit test
+# targets so we can ensure they are built
+# before trying to run them.
+define_property(GLOBAL
+  PROPERTY KLEE_UNIT_TEST_TARGETS
+  BRIEF_DOCS "KLEE unit tests"
+  FULL_DOCS "KLEE unit tests"
+)
+
+set(GTEST_INCLUDE_DIR "${GTEST_SRC_DIR}/include")
+
+if (NOT IS_DIRECTORY "${GTEST_INCLUDE_DIR}")
+  message(FATAL_ERROR
+    "Cannot find GTest include directory \"${GTEST_INCLUDE_DIR}\"")
+endif()
+
+function(add_klee_unit_test target_name)
+  add_executable(${target_name} ${ARGN})
+  target_link_libraries(${target_name} PRIVATE gtest_main)
+  target_include_directories(${target_name} BEFORE PRIVATE "${GTEST_INCLUDE_DIR}")
+  set_target_properties(${target_name}
+    PROPERTIES
+    RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/unittests/"
+  )
+  set_property(GLOBAL
+    APPEND
+    PROPERTY KLEE_UNIT_TEST_TARGETS
+    ${target_name}
+  )
+endfunction()
+
+# Unit Tests
+add_subdirectory(Assignment)
+add_subdirectory(Expr)
+add_subdirectory(Ref)
+add_subdirectory(Solver)
+
+# Set up lit configuration
+set (UNIT_TEST_EXE_SUFFIX "Test")
+configure_file(lit-unit-tests-common.site.cfg.in
+  ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg
+  @ONLY)
+
+# Add a target to run all the unit tests using lit
+get_property(UNIT_TEST_DEPENDS
+  GLOBAL
+  PROPERTY KLEE_UNIT_TEST_TARGETS
+)
+add_custom_target(unittests
+  COMMAND
+    "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
+    DEPENDS ${UNIT_TEST_DEPENDS}
+    COMMENT "Running unittests"
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
diff --git a/unittests/Expr/CMakeLists.txt b/unittests/Expr/CMakeLists.txt
new file mode 100644
index 00000000..4e7bc997
--- /dev/null
+++ b/unittests/Expr/CMakeLists.txt
@@ -0,0 +1,6 @@
+add_klee_unit_test(ExprTest
+  ExprTest.cpp)
+# FIXME: KLEE's libraries should just declare what libraries
+# they depend on so we don't need to manually link.
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(ExprTest PRIVATE kleaverExpr ${LLVM_LIBS})
diff --git a/unittests/Ref/CMakeLists.txt b/unittests/Ref/CMakeLists.txt
new file mode 100644
index 00000000..d678930c
--- /dev/null
+++ b/unittests/Ref/CMakeLists.txt
@@ -0,0 +1,6 @@
+add_klee_unit_test(RefTest
+  RefTest.cpp)
+# FIXME: KLEE's libraries should just declare what libraries
+# they depend on so we don't need to manually link.
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(RefTest PRIVATE kleaverExpr ${LLVM_LIBS})
diff --git a/unittests/Solver/CMakeLists.txt b/unittests/Solver/CMakeLists.txt
new file mode 100644
index 00000000..602a1196
--- /dev/null
+++ b/unittests/Solver/CMakeLists.txt
@@ -0,0 +1,12 @@
+add_klee_unit_test(SolverTest
+  SolverTest.cpp)
+# FIXME: KLEE's libraries should just declare what libraries
+# they depend on so we don't need to manually link.
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(SolverTest
+  PRIVATE
+  kleaverSolver
+  kleaverExpr
+  kleeSupport
+  kleeBasic
+  ${LLVM_LIBS})
diff --git a/unittests/lit-unit-tests-common.cfg b/unittests/lit-unit-tests-common.cfg
new file mode 100644
index 00000000..57663ff7
--- /dev/null
+++ b/unittests/lit-unit-tests-common.cfg
@@ -0,0 +1,11 @@
+# Configuration file for the 'lit' test runner.
+
+import os
+
+import lit.formats
+
+# suffixes: A list of file extensions to treat as test files.
+config.suffixes = []
+
+# testFormat: The test format to use to interpret tests.
+config.test_format = lit.formats.GoogleTest('.', config.unit_test_exe_suffix)
diff --git a/unittests/lit-unit-tests-common.site.cfg.in b/unittests/lit-unit-tests-common.site.cfg.in
new file mode 100644
index 00000000..f106152f
--- /dev/null
+++ b/unittests/lit-unit-tests-common.site.cfg.in
@@ -0,0 +1,9 @@
+import sys
+import os
+
+## @AUTO_GEN_MSG@
+config.name = 'KLEE Unit tests'
+config.unit_test_exe_suffix = "@UNIT_TEST_EXE_SUFFIX@"
+
+# Let the main config do the real work.
+lit_config.load_config(config, "@CMAKE_SOURCE_DIR@/unittests/lit-unit-tests-common.cfg")