CBMC
Public Member Functions | Private Attributes | List of all members
symex_level1t Struct Reference

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

#include <renaming_level.h>

+ Collaboration diagram for symex_level1t:

Public Member Functions

void insert (const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
 Assume ssa is not already known. More...
 
std::optional< std::pair< ssa_exprt, std::size_t > > insert_or_replace (const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
 Set the index for ssa to index. More...
 
bool has (const renamedt< ssa_exprt, L0 > &ssa) const
 
renamedt< ssa_exprt, L1 > operator() (renamedt< ssa_exprt, L0 > l0_expr) const
 
void restore_from (const symex_level1t &other)
 Insert the content of other into this renaming. More...
 

Private Attributes

symex_renaming_levelt current_names
 

Detailed Description

Functor to set the level 1 renaming of SSA expressions.

Level 1 corresponds to function frames. This is to preserve locality in case of recursion

Definition at line 39 of file renaming_level.h.

Member Function Documentation

◆ has()

bool symex_level1t::has ( const renamedt< ssa_exprt, L0 > &  ssa) const
Returns
true if ssa has an associated index

Definition at line 72 of file renaming_level.cpp.

◆ insert()

void symex_level1t::insert ( const renamedt< ssa_exprt, L0 > &  ssa,
std::size_t  index 
)

Assume ssa is not already known.

Definition at line 47 of file renaming_level.cpp.

◆ insert_or_replace()

std::optional< std::pair< ssa_exprt, std::size_t > > symex_level1t::insert_or_replace ( const renamedt< ssa_exprt, L0 > &  ssa,
std::size_t  index 
)

Set the index for ssa to index.

Returns
if an index for ssa was already know, returns it's previous value.

Definition at line 56 of file renaming_level.cpp.

◆ operator()()

renamedt< ssa_exprt, L1 > symex_level1t::operator() ( renamedt< ssa_exprt, L0 >  l0_expr) const
Returns
an SSA expression similar to l0_expr where the L1 tag has been set to the value in current_names of the l1 object identifier of l0_expr

Definition at line 77 of file renaming_level.cpp.

◆ restore_from()

void symex_level1t::restore_from ( const symex_level1t &  other)

Insert the content of other into this renaming.

Definition at line 110 of file renaming_level.cpp.

Member Data Documentation

◆ current_names

symex_renaming_levelt symex_level1t::current_names
private

Definition at line 62 of file renaming_level.h.

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