cprover
symex_renaming_levelt Struct Reference

Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter. More...

#include <renaming_level.h>

+ Inheritance diagram for symex_renaming_levelt:
+ Collaboration diagram for symex_renaming_levelt:

Public Types

typedef std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
 Map identifier to ssa_exprt and counter. More...
 

Public Member Functions

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

Static Public Member Functions

static void increase_counter (const current_namest::iterator &it)
 Increase the counter corresponding to an identifier. More...
 

Public Attributes

current_namest current_names
 

Detailed Description

Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter.

This is extended by the different symex_level structures which are used during symex to ensure static single assignment (SSA) form.

Definition at line 25 of file renaming_level.h.

Member Typedef Documentation

◆ current_namest

typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > symex_renaming_levelt::current_namest

Map identifier to ssa_exprt and counter.

Definition at line 30 of file renaming_level.h.

Constructor & Destructor Documentation

◆ ~symex_renaming_levelt()

virtual symex_renaming_levelt::~symex_renaming_levelt ( )
virtualdefault

Member Function Documentation

◆ current_count()

unsigned symex_renaming_levelt::current_count ( const irep_idt identifier) const
inline

Counter corresponding to an identifier.

Definition at line 34 of file renaming_level.h.

◆ get_variables()

void symex_renaming_levelt::get_variables ( std::unordered_set< ssa_exprt, irep_hash > &  vars) const
inline

Add the ssa_exprt of current_names to vars.

Definition at line 47 of file renaming_level.h.

◆ increase_counter()

static void symex_renaming_levelt::increase_counter ( const current_namest::iterator &  it)
inlinestatic

Increase the counter corresponding to an identifier.

Definition at line 41 of file renaming_level.h.

Member Data Documentation

◆ current_names

current_namest symex_renaming_levelt::current_names

Definition at line 31 of file renaming_level.h.


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