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>
97 std::function<std::size_t(
const irep_idt &)> fresh_l2_name_provider);
118 #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.
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
renamedt< ssa_exprt, L2 > operator()(renamedt< ssa_exprt, L1 > l1_expr) const
Set L2 tag to correspond to the current count of the identifier of l1_expr's.
The type of an expression, extends irept.
void get_variables(const symex_renaming_levelt ¤t_names, std::unordered_set< ssa_exprt, irep_hash > &vars)
Add the ssa_exprt of current_names to vars.
Base class for all expressions.
std::size_t increase_generation(const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this pat...
Class for expressions or types renamed up to a given level.
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.
bool check_renaming(const exprt &expr)
Check that expr is correctly renamed to level 2 and return true in case an error is detected.
bool check_renaming_l1(const exprt &expr)
Check that expr is correctly renamed to level 1 and return true in case an error is detected.
exprt get_original_name(exprt expr)
Undo all levels of renaming.
symex_renaming_levelt current_names
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define SINCE(year, month, day, msg)
nonstd::optional< T > optionalt
Forward depth-first search iterators These iterators' copy operations are expensive,...
symex_renaming_levelt current_names
Functor to set the level 1 renaming of SSA expressions.
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Wrapper for expressions or types which have been renamed up to a given level.