CBMC
|
Replace a symbol expression by a given expression. More...
#include <replace_symbol.h>
Public Types | |
typedef std::unordered_map< irep_idt, exprt > | expr_mapt |
Public Member Functions | |
void | insert (const class symbol_exprt &old_expr, const exprt &new_expr) |
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothing (i.e. More... | |
void | set (const class symbol_exprt &old_expr, const exprt &new_expr) |
Sets old_expr to be replaced by new_expr. More... | |
virtual bool | replace (exprt &dest) const |
virtual bool | replace (typet &dest) const |
void | operator() (exprt &dest) const |
void | operator() (typet &dest) const |
void | clear () |
bool | empty () const |
std::size_t | erase (const irep_idt &id) |
expr_mapt::iterator | erase (expr_mapt::iterator it) |
bool | replaces_symbol (const irep_idt &id) const |
replace_symbolt () | |
virtual | ~replace_symbolt () |
const expr_mapt & | get_expr_map () const |
expr_mapt & | get_expr_map () |
Protected Member Functions | |
virtual bool | replace_symbol_expr (symbol_exprt &dest) const |
bool | have_to_replace (const exprt &dest) const |
bool | have_to_replace (const typet &type) const |
Protected Attributes | |
expr_mapt | expr_map |
std::set< irep_idt > | bindings |
Replace a symbol expression by a given expression.
The type of the symbol must match the type of the replacement. This class is aware of symbol hiding caused by bindings such as forall, exists, and the like.
Definition at line 27 of file replace_symbol.h.
typedef std::unordered_map<irep_idt, exprt> replace_symbolt::expr_mapt |
Definition at line 30 of file replace_symbol.h.
replace_symbolt::replace_symbolt | ( | ) |
Definition at line 16 of file replace_symbol.cpp.
|
virtual |
Definition at line 20 of file replace_symbol.cpp.
|
inline |
Definition at line 54 of file replace_symbol.h.
|
inline |
Definition at line 59 of file replace_symbol.h.
|
inline |
Definition at line 64 of file replace_symbol.h.
|
inline |
Definition at line 69 of file replace_symbol.h.
|
inline |
Definition at line 87 of file replace_symbol.h.
|
inline |
Definition at line 82 of file replace_symbol.h.
|
protected |
Definition at line 164 of file replace_symbol.cpp.
|
protected |
Definition at line 272 of file replace_symbol.cpp.
void replace_symbolt::insert | ( | const class symbol_exprt & | old_expr, |
const exprt & | new_expr | ||
) |
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothing (i.e.
std::map::insert-like behaviour).
Definition at line 24 of file replace_symbol.cpp.
|
inline |
Definition at line 44 of file replace_symbol.h.
|
inline |
Definition at line 49 of file replace_symbol.h.
|
virtual |
Reimplemented in address_of_aware_replace_symbolt, and casting_replace_symbolt.
Definition at line 64 of file replace_symbol.cpp.
|
virtual |
Definition at line 206 of file replace_symbol.cpp.
|
protectedvirtual |
Reimplemented in address_of_aware_replace_symbolt, unchecked_replace_symbolt, and casting_replace_symbolt.
Definition at line 43 of file replace_symbol.cpp.
|
inline |
Definition at line 74 of file replace_symbol.h.
void replace_symbolt::set | ( | const class symbol_exprt & | old_expr, |
const exprt & | new_expr | ||
) |
Sets old_expr to be replaced by new_expr.
Definition at line 36 of file replace_symbol.cpp.
|
mutableprotected |
Definition at line 94 of file replace_symbol.h.
|
protected |
Definition at line 93 of file replace_symbol.h.