cprover
|
#include <goto_symex_state.h>
Public Member Functions | |
void | operator() (ssa_exprt &ssa_expr) |
void | restore_from (const current_namest &other) |
level1t () | |
virtual | ~level1t () |
![]() | |
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 |
Additional Inherited Members | |
![]() | |
typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > > | current_namest |
![]() | |
current_namest | current_names |
Definition at line 97 of file goto_symex_state.h.
|
inline |
Definition at line 122 of file goto_symex_state.h.
|
inlinevirtual |
Definition at line 123 of file goto_symex_state.h.
void goto_symex_statet::level1t::operator() | ( | ssa_exprt & | ssa_expr | ) |
Definition at line 82 of file goto_symex_state.cpp.
References dstringt::empty(), ssa_exprt::get_l1_object_identifier(), ssa_exprt::get_level_1(), and ssa_exprt::set_level_1().
|
inline |
Definition at line 101 of file goto_symex_state.h.
References goto_symex_statet::renaming_levelt::current_names.
Referenced by goto_symext::pop_frame().