CBMC
renamed.h File Reference

Class for expressions or types renamed up to a given level. More...

+ Include dependency graph for renamed.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  renamedt< underlyingt, level >
 Wrapper for expressions or types which have been renamed up to a given level. More...
 

Enumerations

enum  levelt { L0 = 0 , L1 = 1 , L1_WITH_CONSTANT_PROPAGATION = 2 , L2 = 3 }
 Symex renaming level names. More...
 

Functions

template<levelt level>
renamedt< exprt, level > make_renamed (constant_exprt constant)
 
template<levelt level>
void selectively_mutate (renamedt< exprt, level > &renamed, typename renamedt< exprt, level >::mutator_functiont get_mutated_expr)
 This permits replacing subexpressions of the renamed value, so long as each replacement is consistent with our current renaming level (for example, replacing subexpressions of L2 expressions with ones which are themselves L2 renamed). More...
 

Detailed Description

Class for expressions or types renamed up to a given level.

Definition in file renamed.h.

Enumeration Type Documentation

◆ levelt

enum levelt

Symex renaming level names.

Enumerator
L0 
L1 
L1_WITH_CONSTANT_PROPAGATION 
L2 

Definition at line 21 of file renamed.h.

Function Documentation

◆ make_renamed()

template<levelt level>
renamedt<exprt, level> make_renamed ( constant_exprt  constant)

Definition at line 82 of file renamed.h.

◆ selectively_mutate()

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

This permits replacing subexpressions of the renamed value, so long as each replacement is consistent with our current renaming level (for example, replacing subexpressions of L2 expressions with ones which are themselves L2 renamed).

The passed function will be called with each expression node in preorder (i.e. parent expressions before children), and should return an empty optional to make no change or a renamed expression to make a change.

Definition at line 95 of file renamed.h.