Functor to set the level 2 renaming of SSA expressions. More...

Collaboration diagram for symex_level2t:

Public Member Functions
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`. More...

unsigned	latest_index (const irep_idt &identifier) const
	Counter corresponding to an identifier. More...

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

Detailed Description

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.

Member Function Documentation

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: