Fixed initialization of distance to uncovered instructions when KLEE relies on default searchers

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);
 }