12 #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
13 #define CPROVER_GOTO_SYMEX_GOTO_STATE_H
96 const exprt &condition,
Base class for all expressions.
std::size_t size() const
Amount of nodes this expression tree contains.
Container for data that varies per program point, e.g.
std::size_t complexity()
Get the complexity for this state.
goto_statet(const goto_statet &other)=default
goto_statet(guard_managert &guard_manager)
unsigned depth
Distance from entry.
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
void apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
Given a condition that must hold on this path, propagate as much knowledge as possible.
goto_statet(goto_statet &&other)=default
goto_statet & operator=(goto_statet &&other)=default
unsigned atomic_section_id
Threads.
sharing_mapt< irep_idt, exprt > propagation
goto_statet()=delete
Constructors.
const symex_level2t & get_level2() const
goto_statet & operator=(const goto_statet &other)=delete
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
Central data structure: state.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A map implemented as a tree where subtrees can be shared between different maps.
The Boolean constant true.
State type in value_set_domaint, used in value-set analysis and goto-symex.
Local safe pointer analysis.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Functor to set the level 2 renaming of SSA expressions.