diff options
Diffstat (limited to 'lib/Core/Executor.h')
| -rw-r--r-- | lib/Core/Executor.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 852aaf3c..a0174ab7 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -134,10 +134,14 @@ private: std::vector<TimerInfo*> timers; PTree *processTree; + /// Keeps track of all currently ongoing merges. + /// An ongoing merge is a set of states which branched from a single state + /// which ran into a klee_open_merge(), and not all states in the set have + /// reached the corresponding klee_close_merge() yet. 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 + /// ExecutionStates 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 |