From bc84fb1f642cbd15064c86d3839e278be536b254 Mon Sep 17 00:00:00 2001 From: Lukas Wölfer Date: Sat, 24 Jun 2017 19:23:32 +0200 Subject: Added pause and continue functionality for states in Executor --- lib/Core/Executor.cpp | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'lib/Core/Executor.cpp') 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::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::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, -- cgit 1.4.1