diff options
author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2017-06-24 19:31:04 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-15 15:18:36 +0100 |
commit | e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0 (patch) | |
tree | 620bd0ab0ce7f737db5ab7f8f656d32ea0849f4a /lib/Core/Executor.h | |
parent | 0cf0150da0f674c85f9eaccee8b487ed004c3edc (diff) | |
download | klee-e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0.tar.gz |
Implemented incomplete merging
Diffstat (limited to 'lib/Core/Executor.h')
-rw-r--r-- | lib/Core/Executor.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 1bc91be0..852aaf3c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -85,6 +85,7 @@ class Executor : public Interpreter { friend class SpecialFunctionHandler; friend class StatsTracker; friend class MergeHandler; + friend class MergingSearcher; public: class Timer { @@ -133,6 +134,12 @@ private: std::vector<TimerInfo*> timers; PTree *processTree; + std::vector<MergeHandler *> mergeGroups; + + // Set of vectors that are currently paused from scheduling because they are + // waiting to be merged in a klee_close_merge instruction + std::set<ExecutionState *> inCloseMerge; + /// Used to track states that have been added during the current /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. |