cprover
|
#include <goto_symex_state.h>
Public Types | |
typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > > | current_namest |
Public Member Functions | |
virtual | ~renaming_levelt () |
unsigned | current_count (const irep_idt &identifier) const |
void | increase_counter (const irep_idt &identifier) |
void | get_variables (std::unordered_set< ssa_exprt, irep_hash > &vars) const |
Public Attributes | |
current_namest | current_names |
Definition at line 52 of file goto_symex_state.h.
typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > goto_symex_statet::renaming_levelt::current_namest |
Definition at line 56 of file goto_symex_state.h.
|
inlinevirtual |
Definition at line 54 of file goto_symex_state.h.
|
inline |
Definition at line 59 of file goto_symex_state.h.
Referenced by goto_symex_statet::l2_thread_read_encoding(), goto_symext::phi_function(), goto_symex_statet::set_ssa_indices(), goto_symext::symex_assign_symbol(), and goto_symext::symex_atomic_end().
|
inline |
Definition at line 72 of file goto_symex_state.h.
Referenced by goto_symext::phi_function().
|
inline |
Definition at line 66 of file goto_symex_state.h.
Referenced by goto_symex_statet::assignment(), goto_symex_statet::l2_thread_read_encoding(), goto_symext::locality(), goto_symext::symex_dead(), and goto_symext::symex_decl().
current_namest goto_symex_statet::renaming_levelt::current_names |
Definition at line 57 of file goto_symex_state.h.
Referenced by goto_symex_statet::assignment(), goto_symex_statet::l2_thread_read_encoding(), goto_symext::locality(), goto_symext::pop_frame(), goto_symex_statet::level1t::restore_from(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_start_thread(), and goto_symext::trigger_auto_object().