|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <cassert>#include <cstdint>#include <climits>#include <cstdio>#include <cstring>#include <goto-programs/goto_functions.h>#include <goto-symex/state/renaming.h>#include <goto-symex/symex_invariant.h>#include <goto-symex/equation/symex_target.h>#include <pointer-analysis/value_set.h>#include <set>#include <stack>#include <string>#include <irep2/irep2_guard.h>#include <util/base/i2string.h>#include <irep2/irep2.h>#include <memory>#include <vector>#include <goto-symex/waypoint.h>Go to the source code of this file.
Classes | |
| class | goto_symex_statet |
| Class for storing a particular threads state. More... | |
| class | goto_symex_statet::merge_statet |
| Snapshot of the symbolic data needed to merge a deferred path. More... | |
| class | goto_symex_statet::framet |
| Stack frame tracking class. More... | |