about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/CMakeLists.txt63
-rw-r--r--lib/Core/Searcher.cpp2
-rw-r--r--lib/Core/UserSearcher.cpp8
3 files changed, 52 insertions, 21 deletions
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/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index f61ae6ec..c787382f 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -412,6 +412,8 @@ Instruction *MergingSearcher::getMergePoint(ExecutionState &es) {
 }
 
 ExecutionState &MergingSearcher::selectState() {
+  // FIXME: this loop is endless if baseSearcher includes RandomPathSearcher.
+  // The reason is that RandomPathSearcher::removeState() does nothing...
   while (!baseSearcher->empty()) {
     ExecutionState &es = baseSearcher->selectState();
     if (getMergePoint(es)) {
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index fcda26f2..0aa4a4b0 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -117,8 +117,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
 
   // merge support is experimental
   if (UseMerge) {
-    assert(!UseBumpMerge);
-    assert(std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) == CoreSearch.end()); // XXX: needs further debugging: test/Features/Searchers.c fails with this searcher
+    if (UseBumpMerge)
+      klee_error("use-merge and use-bump-merge cannot be used together");
+    // RandomPathSearcher cannot be used in conjunction with MergingSearcher,
+    // see MergingSearcher::selectState() for explanation.
+    if (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end())
+      klee_error("use-merge currently does not support random-path, please use another search strategy");
     searcher = new MergingSearcher(executor, searcher);
   } else if (UseBumpMerge) {
     searcher = new BumpMergingSearcher(executor, searcher);