cprover
|
#include <goto_symex_state.h>
Public Member Functions | |
goto_statet (const goto_symex_statet &s) | |
void | level2_get_variables (std::unordered_set< ssa_exprt, irep_hash > &vars) const |
unsigned | level2_current_count (const irep_idt &identifier) const |
Public Attributes | |
unsigned | depth |
level2t::current_namest | level2_current_names |
value_sett | value_set |
guardt | guard |
symex_targett::sourcet | source |
propagationt | propagation |
unsigned | atomic_section_id |
Definition at line 188 of file goto_symex_state.h.
|
inlineexplicit |
Definition at line 199 of file goto_symex_state.h.
|
inline |
Definition at line 221 of file goto_symex_state.h.
References level2_current_names.
Referenced by goto_symext::phi_function().
|
inline |
Definition at line 211 of file goto_symex_state.h.
References level2_current_names.
Referenced by goto_symext::phi_function().
unsigned goto_symex_statet::goto_statet::atomic_section_id |
Definition at line 197 of file goto_symex_state.h.
Referenced by goto_symext::merge_goto().
unsigned goto_symex_statet::goto_statet::depth |
Definition at line 191 of file goto_symex_state.h.
Referenced by goto_symext::merge_goto().
guardt goto_symex_statet::goto_statet::guard |
Definition at line 194 of file goto_symex_state.h.
Referenced by symex_bmct::merge_goto(), goto_symext::merge_goto(), goto_symext::phi_function(), and goto_symext::symex_goto().
level2t::current_namest goto_symex_statet::goto_statet::level2_current_names |
Definition at line 192 of file goto_symex_state.h.
Referenced by level2_current_count(), and level2_get_variables().
propagationt goto_symex_statet::goto_statet::propagation |
Definition at line 196 of file goto_symex_state.h.
Referenced by goto_symext::phi_function().
symex_targett::sourcet goto_symex_statet::goto_statet::source |
Definition at line 195 of file goto_symex_state.h.
Referenced by symex_bmct::merge_goto().
value_sett goto_symex_statet::goto_statet::value_set |
Definition at line 193 of file goto_symex_state.h.
Referenced by goto_symext::merge_value_sets().