10 files changed, 173 insertions, 101 deletions
diff --git a/README-CMake.md b/README-CMake.md
index 0b9cfd61..991694cd 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -75,6 +75,16 @@ cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src
 
 * `MAKE_BINARY` (STRING) - Path to `make` binary used to build KLEE's runtime.
 
+* `metaSMT_DIR` (STRING) - Provides a hint to CMake, where the metaSMT constraint
+  solver can be found.  This should be an absolute path to a directory
+  containing the file `metaSMTConfig.cmake`.
+
+* `STP_DIR` (STRING) - Provides a hint to CMake, where the STP constraint
+  solver can be found.  This should be an absolute path to a directory
+  containing the file `STPConfig.cmake`. This file is installed by STP
+  but also exists in its build directory. This allows KLEE to link
+  against STP in a build directory or an installed copy.
+
 * `USE_CMAKE_FIND_PACKAGE_LLVM` (BOOLEAN) - Use `find_package(LLVM CONFIG)`
    to find LLVM.
 
diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt
index 13f76d42..d0a309c9 100644
--- a/lib/Basic/CMakeLists.txt
+++ b/lib/Basic/CMakeLists.txt
@@ -7,8 +7,23 @@
 #
 #===------------------------------------------------------------------------===#
 klee_add_component(kleeBasic
-	CmdLineOptions.cpp
-	ConstructSolverChain.cpp
-	KTest.cpp
-	Statistics.cpp
+  CmdLineOptions.cpp
+  ConstructSolverChain.cpp
+  KTest.cpp
+  Statistics.cpp
+)
+set(LLVM_COMPONENTS
+  support
+)
+
+klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
+target_link_libraries(kleeBasic PUBLIC ${LLVM_LIBS})
+
+target_link_libraries(kleeBasic PRIVATE
+  # FIXME: THIS IS STUPID.
+  # `ConstructSolverChain.cpp` should be in
+  # `kleaverSolver` not in in `kleeBasic`.
+  # We are creating a circular dependency because
+  # of this because `kleaverSolver` depends on `kleeBasic`.
+  kleaverSolver
 )
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 05e2cffa..86ce3cfc 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -7,23 +7,48 @@
 #
 #===------------------------------------------------------------------------===#
 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
+  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
+)
+
+# TODO: Work out what the correct LLVM components are for
+# kleeCore.
+set(LLVM_COMPONENTS
+  core
+  support
+)
+
+if ("${LLVM_PACKAGE_VERSION}" VERSION_EQUAL "3.6" OR
+    "${LLVM_PACKAGE_VERSION}" VERSION_GREATER "3.6")
+  list(APPEND LLVM_COMPONENTS mcjit executionengine native)
+else()
+  list(APPEND LLVM_COMPONENTS jit engine)
+endif()
+
+
+klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
+target_link_libraries(kleeCore PUBLIC ${LLVM_LIBS})
+target_link_libraries(kleeCore PRIVATE
+  kleeBasic
+  kleeModule
+  kleaverSolver
+  kleaverExpr
+  kleeSupport
 )
diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt
index 6ea77544..4c63fe5b 100644
--- a/lib/Expr/CMakeLists.txt
+++ b/lib/Expr/CMakeLists.txt
@@ -7,17 +7,23 @@
 #
 #===------------------------------------------------------------------------===#
 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
+  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
 )
+
+set(LLVM_COMPONENTS
+  support
+)
+klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
+target_link_libraries(kleaverExpr PUBLIC ${LLVM_LIBS})
diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt
index a952ed17..22fd3c07 100644
--- a/lib/Module/CMakeLists.txt
+++ b/lib/Module/CMakeLists.txt
@@ -7,14 +7,29 @@
 #
 #===------------------------------------------------------------------------===#
 klee_add_component(kleeModule
-	Checks.cpp
-	InstructionInfoTable.cpp
-	IntrinsicCleaner.cpp
-	KInstruction.cpp
-	KModule.cpp
-	LowerSwitch.cpp
-	ModuleUtil.cpp
-	Optimize.cpp
-	PhiCleaner.cpp
-	RaiseAsm.cpp
+  Checks.cpp
+  InstructionInfoTable.cpp
+  IntrinsicCleaner.cpp
+  KInstruction.cpp
+  KModule.cpp
+  LowerSwitch.cpp
+  ModuleUtil.cpp
+  Optimize.cpp
+  PhiCleaner.cpp
+  RaiseAsm.cpp
 )
+
+set(LLVM_COMPONENTS
+  bitreader
+  bitwriter
+  ipo
+  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})
+target_link_libraries(kleeModule PUBLIC ${LLVM_LIBS})
diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt
index 8add4ad6..20da74da 100644
--- a/lib/Solver/CMakeLists.txt
+++ b/lib/Solver/CMakeLists.txt
@@ -7,26 +7,37 @@
 #
 #===------------------------------------------------------------------------===#
 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
+  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})
+set(LLVM_COMPONENTS
+  support
+)
+klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
+target_link_libraries(kleaverSolver PUBLIC ${LLVM_LIBS})
+
+target_link_libraries(kleaverSolver PRIVATE
+  kleeBasic
+  kleaverExpr
+  kleeSupport
+  ${KLEE_SOLVER_LIBRARIES})
+
diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt
index 4bf7ea7d..4e44fbc6 100644
--- a/lib/Support/CMakeLists.txt
+++ b/lib/Support/CMakeLists.txt
@@ -7,14 +7,20 @@
 #
 #===------------------------------------------------------------------------===#
 klee_add_component(kleeSupport
-	CompressionStream.cpp
-	ErrorHandling.cpp
-	MemoryUsage.cpp
-	PrintVersion.cpp
-	RNG.cpp
-	Time.cpp
-	Timer.cpp
-	TreeStream.cpp
+  CompressionStream.cpp
+  ErrorHandling.cpp
+  MemoryUsage.cpp
+  PrintVersion.cpp
+  RNG.cpp
+  Time.cpp
+  Timer.cpp
+  TreeStream.cpp
 )
 
 target_link_libraries(kleeSupport PRIVATE ${ZLIB_LIBRARIES})
+
+set(LLVM_COMPONENTS
+  support
+)
+klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
+target_link_libraries(kleeSupport PUBLIC ${LLVM_LIBS})
diff --git a/tools/gen-random-bout/CMakeLists.txt b/tools/gen-random-bout/CMakeLists.txt
index d1fa6b09..c4596bc9 100644
--- a/tools/gen-random-bout/CMakeLists.txt
+++ b/tools/gen-random-bout/CMakeLists.txt
@@ -7,7 +7,7 @@
 #
 #===------------------------------------------------------------------------===#
 add_executable(gen-random-bout
-	gen-random-bout.cpp
+  gen-random-bout.cpp
 )
 
 set(KLEE_LIBS kleeBasic)
diff --git a/tools/kleaver/CMakeLists.txt b/tools/kleaver/CMakeLists.txt
index befbcc6e..c079c2a4 100644
--- a/tools/kleaver/CMakeLists.txt
+++ b/tools/kleaver/CMakeLists.txt
@@ -7,12 +7,13 @@
 #
 #===------------------------------------------------------------------------===#
 add_executable(kleaver
-	main.cpp
+  main.cpp
 )
 
-klee_get_llvm_libs(LLVM_LIBS support)
-set(KLEE_LIBS kleeBasic kleaverSolver kleaverExpr kleeSupport)
+set(KLEE_LIBS
+  kleaverSolver
+)
 
-target_link_libraries(kleaver ${KLEE_LIBS} ${LLVM_LIBS})
+target_link_libraries(kleaver ${KLEE_LIBS})
 
 install(TARGETS kleaver RUNTIME DESTINATION bin)
diff --git a/tools/klee/CMakeLists.txt b/tools/klee/CMakeLists.txt
index b6e907ab..8b05c357 100644
--- a/tools/klee/CMakeLists.txt
+++ b/tools/klee/CMakeLists.txt
@@ -7,31 +7,14 @@
 #
 #===------------------------------------------------------------------------===#
 add_executable(klee
-	main.cpp
+  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
+set(KLEE_LIBS
+  kleeCore
 )
 
-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})
+target_link_libraries(klee ${KLEE_LIBS})
 
 install(TARGETS klee RUNTIME DESTINATION bin)