diff options
| author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2018-04-05 15:56:05 +0200 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-15 15:18:36 +0100 |
| commit | 8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e (patch) | |
| tree | 6228802a03ce503879b4e41ce643912afe512f04 /lib/Core/Executor.h | |
| parent | e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0 (diff) | |
| download | klee-8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e.tar.gz | |
Improved code quality
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 |