about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2020-10-07 17:46:13 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-10-12 11:31:05 +0100
commitb196bd4a9cfc4ae9d582fc3d17c15094287bb36f (patch)
tree846250ca8f2f983d0caf6cae7f0db269f92a33f9
parent8cb0d545138cbb876318ed6d578b2b6a6a92b81a (diff)
downloadklee-b196bd4a9cfc4ae9d582fc3d17c15094287bb36f.tar.gz
Searcher: remove addState/removeState functions
-rw-r--r--lib/Core/Searcher.cpp2
-rw-r--r--lib/Core/Searcher.h20
2 files changed, 6 insertions, 16 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index e2f11a87..f8fd2aea 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -420,7 +420,7 @@ void IterativeDeepeningTimeSearcher::update(
           removedStates.end() &&
       elapsed > time) {
     pausedStates.insert(current);
-    baseSearcher->removeState(current);
+    baseSearcher->update(nullptr, {}, {current});
   }
 
   // no states left in underlying searcher: fill with paused states
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 9243b69a..e7f146e0 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -62,16 +62,6 @@ namespace klee {
       os << "<unnamed searcher>\n";
     }
 
-    // utility functions
-
-    void addState(ExecutionState *es, ExecutionState *current = nullptr) {
-      update(current, {es}, std::vector<ExecutionState *>());
-    }
-
-    void removeState(ExecutionState *es, ExecutionState *current = nullptr) {
-      update(current, std::vector<ExecutionState *>(), {es});
-    }
-
     enum CoreSearchType : std::uint8_t {
       DFS,
       BFS,
@@ -259,18 +249,18 @@ namespace klee {
     /// Remove state from the searcher chain, while keeping it in the executor.
     /// This is used here to 'freeze' a state while it is waiting for other
     /// states in its merge group to reach the same instruction.
-    void pauseState(ExecutionState &state){
+    void pauseState(ExecutionState &state) {
       assert(std::find(pausedStates.begin(), pausedStates.end(), &state) == pausedStates.end());
       pausedStates.push_back(&state);
-      baseSearcher->removeState(&state);
+      baseSearcher->update(nullptr, {}, {&state});
     }
 
     /// Continue a paused state
-    void continueState(ExecutionState &state){
+    void continueState(ExecutionState &state) {
       auto it = std::find(pausedStates.begin(), pausedStates.end(), &state);
-      assert( it != pausedStates.end());
+      assert(it != pausedStates.end());
       pausedStates.erase(it);
-      baseSearcher->addState(&state);
+      baseSearcher->update(nullptr, {&state}, {});
     }
 
     ExecutionState &selectState() override;