aboutsummaryrefslogtreecommitdiffhomepage
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;