cprover
|
#include <goto_symex_state.h>
Public Member Functions | |
void | operator() (ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) |
level0t () | |
virtual | ~level0t () |
![]() | |
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 98 of file goto_symex_state.h.
|
inline |
Definition at line 105 of file goto_symex_state.h.
|
inlinevirtual |
Definition at line 106 of file goto_symex_state.h.
void goto_symex_statet::level0t::operator() | ( | ssa_exprt & | ssa_expr, |
const namespacet & | ns, | ||
unsigned | thread_nr | ||
) |
Definition at line 37 of file goto_symex_state.cpp.
References DATA_INVARIANT, dstringt::empty(), ssa_exprt::get_level_0(), ssa_exprt::get_object_name(), irept::id(), id2string(), symbolt::is_shared(), namespacet::lookup(), ssa_exprt::set_level_0(), and symbolt::type.