cprover
symex_level2t Struct Reference

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

#include <renaming_level.h>

+ Collaboration diagram for symex_level2t:

Public Member Functions

renamedt< ssa_exprt, L2operator() (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...
 

Public Attributes

symex_renaming_levelt current_names
 

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 81 of file renaming_level.h.

Member Function Documentation

◆ increase_generation()

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 148 of file renaming_level.cpp.

◆ latest_index()

unsigned symex_level2t::latest_index ( const irep_idt identifier) const

Counter corresponding to an identifier.

Definition at line 142 of file renaming_level.cpp.

◆ operator()()

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 113 of file renaming_level.cpp.

Member Data Documentation

◆ current_names

symex_renaming_levelt symex_level2t::current_names

Definition at line 83 of file renaming_level.h.


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