diff options
author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2017-06-24 19:23:32 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-11-30 12:18:15 +0000 |
commit | bc84fb1f642cbd15064c86d3839e278be536b254 (patch) | |
tree | 316c6a71c8eb894ea9d7b05e0ffbf88273cac961 /lib/Core/Executor.h | |
parent | fb01144ad362210e088a27e21c062ecd16b3f097 (diff) | |
download | klee-bc84fb1f642cbd15064c86d3839e278be536b254.tar.gz |
Added pause and continue functionality for states in Executor
Diffstat (limited to 'lib/Core/Executor.h')
-rw-r--r-- | lib/Core/Executor.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 27cefcc0..c6f01179 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -144,6 +144,13 @@ private: /// \invariant \ref addedStates and \ref removedStates are disjoint. std::vector<ExecutionState *> removedStates; + /// Used to track states that are not terminated, but should not + /// be scheduled by the searcher. + std::vector<ExecutionState *> pausedStates; + /// States that were 'paused' from scheduling, that now may be + /// scheduled again + std::vector<ExecutionState *> continuedStates; + /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order /// (outside the normal search interface) until they terminate. When @@ -389,6 +396,10 @@ private: bool shouldExitOn(enum TerminateReason termReason); + // remove state from searcher only + void pauseState(ExecutionState& state); + // add state to searcher only + void continueState(ExecutionState& state); // remove state from queue and delete void terminateState(ExecutionState &state); // call exit handler and terminate state |