cprover
symex_level1t Struct Reference

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

#include <renaming_level.h>

+ Inheritance diagram for symex_level1t:
+ Collaboration diagram for symex_level1t:

Public Member Functions

void operator() (ssa_exprt &ssa_expr)
 
void restore_from (const current_namest &other)
 Insert the content of other into this renaming. More...
 
 symex_level1t ()=default
 
 ~symex_level1t () override=default
 
- Public Member Functions inherited from symex_renaming_levelt
virtual ~symex_renaming_levelt ()=default
 
unsigned current_count (const irep_idt &identifier) const
 Counter corresponding to an identifier. More...
 
void get_variables (std::unordered_set< ssa_exprt, irep_hash > &vars) const
 Add the ssa_exprt of current_names to vars. More...
 

Additional Inherited Members

- Public Types inherited from symex_renaming_levelt
typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
 Map identifier to ssa_exprt and counter. More...
 
- Static Public Member Functions inherited from symex_renaming_levelt
static void increase_counter (const current_namest::iterator &it)
 Increase the counter corresponding to an identifier. More...
 
- Public Attributes inherited from symex_renaming_levelt
current_namest 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 69 of file renaming_level.h.

Constructor & Destructor Documentation

◆ symex_level1t()

symex_level1t::symex_level1t ( )
default

◆ ~symex_level1t()

symex_level1t::~symex_level1t ( )
overridedefault

Member Function Documentation

◆ operator()()

void symex_level1t::operator() ( ssa_exprt ssa_expr)

Definition at line 43 of file renaming_level.cpp.

◆ restore_from()

void symex_level1t::restore_from ( const current_namest other)

Insert the content of other into this renaming.

Definition at line 59 of file renaming_level.cpp.


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