cprover
symex_level0t Struct Reference

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

#include <renaming_level.h>

+ Inheritance diagram for symex_level0t:
+ Collaboration diagram for symex_level0t:

Public Member Functions

void operator() (ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
 
 symex_level0t ()=default
 
 ~symex_level0t () 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 0 renaming of SSA expressions.

Level 0 corresponds to threads. The renaming is built for one particular interleaving.

Definition at line 57 of file renaming_level.h.

Constructor & Destructor Documentation

◆ symex_level0t()

symex_level0t::symex_level0t ( )
default

◆ ~symex_level0t()

symex_level0t::~symex_level0t ( )
overridedefault

Member Function Documentation

◆ operator()()

void symex_level0t::operator() ( ssa_exprt ssa_expr,
const namespacet ns,
unsigned  thread_nr 
)

Definition at line 19 of file renaming_level.cpp.


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