CBMC
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Friends | List of all members
renamedt< underlyingt, level > Class Template Reference

Wrapper for expressions or types which have been renamed up to a given level. More...

#include <renamed.h>

+ Inheritance diagram for renamedt< underlyingt, level >:
+ Collaboration diagram for renamedt< underlyingt, level >:

Public Member Functions

const underlyingt & get () const
 
void simplify (simplify_exprt &simplifier)
 

Private Member Functions

underlyingt & value ()
 
 renamedt (underlyingt value)
 Only the friend classes can create renamedt objects.
 

Friends

struct symex_level1t
 
struct symex_level2t
 
class goto_symex_statet
 
renamedt< ssa_exprt, L0 > symex_level0 (ssa_exprt, const namespacet &, std::size_t)
 Set the level 0 renaming of SSA expressions.
 

Detailed Description

template<typename underlyingt, levelt level>
class renamedt< underlyingt, level >

Wrapper for expressions or types which have been renamed up to a given level.

Definition at line 32 of file renamed.h.

Constructor & Destructor Documentation

◆ renamedt()

template<typename underlyingt , levelt level>
renamedt< underlyingt, level >::renamedt ( underlyingt  value)
inlineexplicitprivate

Only the friend classes can create renamedt objects.

Definition at line 63 of file renamed.h.

Member Function Documentation

◆ get()

template<typename underlyingt , levelt level>
const underlyingt & renamedt< underlyingt, level >::get ( ) const
inline

Definition at line 40 of file renamed.h.

◆ simplify()

template<typename underlyingt , levelt level>
void renamedt< underlyingt, level >::simplify ( simplify_exprt &  simplifier)
inline

Definition at line 45 of file renamed.h.

◆ value()

template<typename underlyingt , levelt level>
underlyingt & renamedt< underlyingt, level >::value ( )
inlineprivate

Definition at line 51 of file renamed.h.

Friends And Related Symbol Documentation

◆ goto_symex_statet

template<typename underlyingt , levelt level>
friend class goto_symex_statet
friend

Definition at line 60 of file renamed.h.

◆ symex_level0

template<typename underlyingt , levelt level>
renamedt< ssa_exprt, L0 > symex_level0 ( ssa_exprt  ,
const namespacet &  ,
std::size_t   
)
friend

Set the level 0 renaming of SSA expressions.

Level 0 corresponds to threads. The renaming is built for one particular interleaving. Rename ssa_expr using thread_nr as L0 tag, unless ssa_expr is a guard, a shared variable or a function. ns is queried to decide whether we are in one of these cases.

Definition at line 22 of file renaming_level.cpp.

◆ symex_level1t

template<typename underlyingt , levelt level>
friend struct symex_level1t
friend

Definition at line 58 of file renamed.h.

◆ symex_level2t

template<typename underlyingt , levelt level>
friend struct symex_level2t
friend

Definition at line 59 of file renamed.h.

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