cprover
symex_level2t Struct Reference

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

#include <renaming_level.h>

+ Inheritance diagram for symex_level2t:
+ Collaboration diagram for symex_level2t:

Public Member Functions

 symex_level2t ()=default
 
 ~symex_level2t () 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 2 renaming of SSA expressions.

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

Definition at line 83 of file renaming_level.h.

Constructor & Destructor Documentation

◆ symex_level2t()

symex_level2t::symex_level2t ( )
default

◆ ~symex_level2t()

symex_level2t::~symex_level2t ( )
overridedefault

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