12#ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
13#define CPROVER_GOTO_SYMEX_GOTO_STATE_H
91 const exprt &condition,
Base class for all expressions.
goto_statet & operator=(goto_statet &&other)=default
goto_statet(const goto_statet &other)=default
goto_statet & operator=(const goto_statet &other)=delete
goto_statet(guard_managert &guard_manager)
unsigned depth
Distance from entry.
bool reachable
Is this code reachable?
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
unsigned atomic_section_id
Threads.
sharing_mapt< irep_idt, exprt > propagation
goto_statet()=delete
Constructors.
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.
sharing_mapt< exprt, symbol_exprt, false, irep_hash > dereference_cache
This is used for eliminating repeated complicated dereferences.
const symex_level2t & get_level2() const
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.
guard_expr_managert guard_managert
Functor to set the level 2 renaming of SSA expressions.