diff options
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/CMakeLists.txt | 63 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 2 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 8 |
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); |