goto_symex_statet::level1t Struct Reference

#include <goto_symex_state.h>

Inheritance diagram for goto_symex_statet::level1t:

Collaboration diagram for goto_symex_statet::level1t:

Public Member Functions
void	operator() (ssa_exprt &ssa_expr)
void	restore_from (const current_namest &other)
	level1t ()
virtual	~level1t ()
Public Member Functions inherited from goto_symex_statet::renaming_levelt
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
Public Types inherited from goto_symex_statet::renaming_levelt
typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > >	current_namest
Public Attributes inherited from goto_symex_statet::renaming_levelt
current_namest	current_names

Detailed Description

Definition at line 97 of file goto_symex_state.h.

Constructor & Destructor Documentation

level1t()

goto_symex_statet::level1t::level1t ( )

inline

Definition at line 122 of file goto_symex_state.h.

~level1t()

virtual goto_symex_statet::level1t::~level1t ( )

inlinevirtual

Definition at line 123 of file goto_symex_state.h.

Member Function Documentation

operator()()

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().

restore_from()

void goto_symex_statet::level1t::restore_from ( const current_namest &  other )

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().

---

The documentation for this struct was generated from the following files:

• goto-symex/goto_symex_state.h
• goto-symex/goto_symex_state.cpp