#include <algorithm>
#include <deque>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/state/goto_symex_state.h>
#include <goto-symex/state/renaming.h>
#include <goto-symex/equation/symex_target.h>
#include <list>
#include <map>
#include <memory>
#include <optional>
#include <set>
#include <irep2/irep2.h>
#include <util/message/message.h>
#include <util/irep/std_expr.h>

Include dependency graph for execution_state.h:

This graph shows which files directly or indirectly include this file:

Classes
class	execution_statet
	Thread-aware symex state explored by reachability_treet. More...
struct	execution_statet::parked_patht
	A path the transition parked for a deferred merge: the sibling arm of a branch, or the continuation a return parked at end_of_function. More...
struct	execution_statet::transition_resultt
class	execution_statet::ex_state_level2t
	execution_statet specific level2t. More...
class	execution_statet::state_hashing_level2t
	State-hashing level2t. More...
struct	execution_statet::transition_footprintt
	The objects one transition read and wrote, as MPOR records them. More...
class	dfs_execution_statet
	Execution state for DFS thread exploration. More...
class	schedule_execution_statet
	Execution state class for –schedule exploration. More...

Classes