diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r-- | lib/Core/Executor.cpp | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0b7aa1a9..e79d6a2c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2456,6 +2456,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { void Executor::updateStates(ExecutionState *current) { if (searcher) { searcher->update(current, addedStates, removedStates); + searcher->update(0, continuedStates, pausedStates); + pausedStates.clear(); + continuedStates.clear(); } states.insert(addedStates.begin(), addedStates.end()); @@ -2741,6 +2744,31 @@ std::string Executor::getAddressInfo(ExecutionState &state, return info.str(); } +void Executor::pauseState(ExecutionState &state){ + std::vector<ExecutionState *>::iterator it = std::find(continuedStates.begin(), continuedStates.end(), &state); + // If the state was to be continued, but now gets paused again + if (it != continuedStates.end()){ + // ...just don't continue it + std::swap(*it, continuedStates.back()); + continuedStates.pop_back(); + } else { + pausedStates.push_back(&state); + } +} + +void Executor::continueState(ExecutionState &state){ + std::vector<ExecutionState *>::iterator it = std::find(pausedStates.begin(), pausedStates.end(), &state); + // If the state was to be paused, but now gets continued again + if (it != pausedStates.end()){ + // ...don't pause it + std::swap(*it, pausedStates.back()); + pausedStates.pop_back(); + } else { + continuedStates.push_back(&state); + } +} + + void Executor::terminateState(ExecutionState &state) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, |