CBMC
Public Types | 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 Types

using mutator_functiont = std::function< optionalt< renamedt >(const renamedt &)>
 

Public Member Functions

const underlyingt & get () const
 
void simplify (const namespacet &ns)
 

Private Member Functions

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

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. More...
 
template<levelt make_renamed_level>
renamedt< exprt, make_renamed_level > make_renamed (constant_exprt constant)
 
template<levelt selectively_mutate_level>
void selectively_mutate (renamedt< exprt, selectively_mutate_level > &renamed, typename renamedt< exprt, selectively_mutate_level >::mutator_functiont get_mutated_expr)
 

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.

Member Typedef Documentation

◆ mutator_functiont

template<typename underlyingt , levelt level>
using renamedt< underlyingt, level >::mutator_functiont = std::function<optionalt<renamedt>(const renamedt &)>

Definition at line 51 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 76 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 ( const namespacet &  ns)
inline

Definition at line 45 of file renamed.h.

◆ value()

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

Definition at line 54 of file renamed.h.

Friends And Related Function Documentation

◆ goto_symex_statet

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

Definition at line 63 of file renamed.h.

◆ make_renamed

template<typename underlyingt , levelt level>
template<levelt make_renamed_level>
renamedt<exprt, make_renamed_level> make_renamed ( constant_exprt  constant)
friend

Definition at line 82 of file renamed.h.

◆ selectively_mutate

template<typename underlyingt , levelt level>
template<levelt selectively_mutate_level>
void selectively_mutate ( renamedt< exprt, selectively_mutate_level > &  renamed,
typename renamedt< exprt, selectively_mutate_level >::mutator_functiont  get_mutated_expr 
)
friend

◆ 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 61 of file renamed.h.

◆ symex_level2t

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

Definition at line 62 of file renamed.h.

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