cprover
|
Wrapper for a current_names
map, which maps each identifier to an SSA expression and a counter.
More...
#include <renaming_level.h>
Public Types | |
typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > > | current_namest |
Map identifier to ssa_exprt and counter. More... | |
Public Member Functions | |
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... | |
Static Public Member Functions | |
static void | increase_counter (const current_namest::iterator &it) |
Increase the counter corresponding to an identifier. More... | |
Public Attributes | |
current_namest | current_names |
Wrapper for a current_names
map, which maps each identifier to an SSA expression and a counter.
This is extended by the different symex_level structures which are used during symex to ensure static single assignment (SSA) form.
Definition at line 25 of file renaming_level.h.
typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > symex_renaming_levelt::current_namest |
Map identifier to ssa_exprt and counter.
Definition at line 30 of file renaming_level.h.
|
virtualdefault |
|
inline |
Counter corresponding to an identifier.
Definition at line 34 of file renaming_level.h.
|
inline |
Add the ssa_exprt
of current_names to vars.
Definition at line 47 of file renaming_level.h.
|
inlinestatic |
Increase the counter corresponding to an identifier.
Definition at line 41 of file renaming_level.h.
current_namest symex_renaming_levelt::current_names |
Definition at line 31 of file renaming_level.h.