Public Member Functions

Set L2 tag to correspond to the current count of the identifier of l1_expr's.

Counter corresponding to an identifier.

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 path.

Public Attributes

Functor to set the level 2 renaming of SSA expressions.

Level 2 corresponds to SSA. This is to ensure each variable is only assigned once.

Definition at line 68 of file renaming_level.h.

std::size_t symex_level2t::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 path.

Definition at line 137 of file renaming_level.cpp.

unsigned symex_level2t::latest_index ( const irep_idt & identifier ) const

Counter corresponding to an identifier.

Definition at line 131 of file renaming_level.cpp.

renamedt< ssa_exprt, L2 > symex_level2t::operator() ( renamedt< ssa_exprt, L1 > l1_expr ) const

Set L2 tag to correspond to the current count of the identifier of l1_expr's.

Definition at line 101 of file renaming_level.cpp.

symex_renaming_levelt symex_level2t::current_names

Definition at line 70 of file renaming_level.h.

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