cprover
|
Functor to set the level 1 renaming of SSA expressions. More...
#include <renaming_level.h>
Public Member Functions | |
void | operator() (ssa_exprt &ssa_expr) |
void | restore_from (const current_namest &other) |
Insert the content of other into this renaming. More... | |
symex_level1t ()=default | |
~symex_level1t () override=default | |
![]() | |
virtual | ~symex_renaming_levelt ()=default |
unsigned | current_count (const irep_idt &identifier) const |
Counter corresponding to an identifier. More... | |
void | get_variables (std::unordered_set< ssa_exprt, irep_hash > &vars) const |
Add the ssa_exprt of current_names to vars. More... | |
Additional Inherited Members | |
![]() | |
typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > > | current_namest |
Map identifier to ssa_exprt and counter. More... | |
![]() | |
static void | increase_counter (const current_namest::iterator &it) |
Increase the counter corresponding to an identifier. More... | |
![]() | |
current_namest | current_names |
Functor to set the level 1 renaming of SSA expressions.
Level 1 corresponds to function frames. This is to preserve locality in case of recursion
Definition at line 69 of file renaming_level.h.
|
default |
|
overridedefault |
void symex_level1t::operator() | ( | ssa_exprt & | ssa_expr | ) |
Definition at line 43 of file renaming_level.cpp.
void symex_level1t::restore_from | ( | const current_namest & | other | ) |
Insert the content of other
into this renaming.
Definition at line 59 of file renaming_level.cpp.