aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp2
-rw-r--r--lib/Core/UserSearcher.cpp14
-rw-r--r--lib/Core/UserSearcher.h2
3 files changed, 12 insertions, 6 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index a0a6f7ea..673476f6 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -352,6 +352,8 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
this->solver = new TimingSolver(solver, EqualitySubstitution);
memory = new MemoryManager(&arrayCache);
+ initializeSearchOptions();
+
if (DebugPrintInstructions.isSet(FILE_ALL) ||
DebugPrintInstructions.isSet(FILE_COMPACT) ||
DebugPrintInstructions.isSet(FILE_SRC)) {
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 4275f3a5..6158f722 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -55,6 +55,14 @@ namespace {
}
+void klee::initializeSearchOptions() {
+ // default values
+ if (CoreSearch.empty()) {
+ CoreSearch.push_back(Searcher::RandomPath);
+ CoreSearch.push_back(Searcher::NURS_CovNew);
+ }
+}
+
bool klee::userSearcherRequiresMD2U() {
return (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_MD2U) != CoreSearch.end() ||
std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_CovNew) != CoreSearch.end() ||
@@ -84,12 +92,6 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
Searcher *klee::constructUserSearcher(Executor &executor) {
- // default values
- if (CoreSearch.size() == 0) {
- CoreSearch.push_back(Searcher::RandomPath);
- CoreSearch.push_back(Searcher::NURS_CovNew);
- }
-
Searcher *searcher = getNewSearcher(CoreSearch[0], executor);
if (CoreSearch.size() > 1) {
diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h
index d01a017f..1c04581d 100644
--- a/lib/Core/UserSearcher.h
+++ b/lib/Core/UserSearcher.h
@@ -17,6 +17,8 @@ namespace klee {
// XXX gross, should be on demand?
bool userSearcherRequiresMD2U();
+ void initializeSearchOptions();
+
Searcher *constructUserSearcher(Executor &executor);
}