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