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< std::optional< 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.
Member Typedef Documentation
◆ mutator_functiont
template<typename underlyingt , levelt level>
| using renamedt< underlyingt, level >::mutator_functiont = std::function<std::optional<renamedt>(const renamedt &)> |
Constructor & Destructor Documentation
◆ renamedt()
Member Function Documentation
◆ get()
template<typename underlyingt , levelt level>
|
inline |
◆ simplify()
template<typename underlyingt , levelt level>
|
inline |
◆ value()
template<typename underlyingt , levelt level>
|
inlineprivate |
Friends And Related Function Documentation
◆ goto_symex_statet
template<typename underlyingt , levelt level>
|
friend |
◆ make_renamed
template<typename underlyingt , levelt level>
template<levelt make_renamed_level>
|
friend |
◆ selectively_mutate
template<typename underlyingt , levelt level>
template<levelt selectively_mutate_level>
|
friend |
◆ symex_level0
template<typename underlyingt , levelt level>
|
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 |
◆ symex_level2t
template<typename underlyingt , levelt level>
|
friend |
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-symex/renamed.h
