Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
13 #define CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
16 #include <unordered_set>
47 void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars)
const
50 vars.insert(pair.second.first);
89 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
~symex_level1t() override=default
void operator()(ssa_exprt &ssa_expr)
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
Add the ssa_exprt of current_names to vars.
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
Map identifier to ssa_exprt and counter.
~symex_level0t() override=default
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
Expression providing an SSA-renamed symbol of expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Functor to set the level 2 renaming of SSA expressions.
~symex_level2t() override=default
virtual ~symex_renaming_levelt()=default
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter.
Functor to set the level 0 renaming of SSA expressions.
void restore_from(const current_namest &other)
Insert the content of other into this renaming.
Functor to set the level 1 renaming of SSA expressions.
current_namest current_names