cprover
Loading...
Searching...
No Matches
address_of_aware_replace_symbolt Class Reference

Replace symbols with constants while maintaining syntactically valid expressions. More...

#include <replace_symbol.h>

Inheritance diagram for address_of_aware_replace_symbolt:
Collaboration diagram for address_of_aware_replace_symbolt:

Classes

class  set_require_lvalue_and_backupt

Public Member Functions

bool replace (exprt &dest) const override
Public Member Functions inherited from unchecked_replace_symbolt
 unchecked_replace_symbolt ()
void insert (const symbol_exprt &old_expr, const exprt &new_expr)
Public Member Functions inherited from replace_symbolt
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.
void set (const class symbol_exprt &old_expr, const exprt &new_expr)
 Sets old_expr to be replaced by new_expr.
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_maptget_expr_map () const
expr_maptget_expr_map ()

Private Member Functions

bool replace_symbol_expr (symbol_exprt &dest) const override

Private Attributes

bool require_lvalue = false

Additional Inherited Members

Public Types inherited from replace_symbolt
typedef std::unordered_map< irep_idt, exprtexpr_mapt
Protected Member Functions inherited from unchecked_replace_symbolt
bool replace_symbol_expr (symbol_exprt &dest) const override
Protected Member Functions inherited from replace_symbolt
bool have_to_replace (const exprt &dest) const
bool have_to_replace (const typet &type) const
Protected Attributes inherited from replace_symbolt
expr_mapt expr_map
std::set< irep_idtbindings

Detailed Description

Replace symbols with constants while maintaining syntactically valid expressions.

If you are replacing symbols with constants in an l-value, you can create something that is not an l-value. For example if your l-value is "a[i]" then substituting i for a constant results in an l-value but substituting a for a constant (array) wouldn't. This only applies to the "top level" of the expression, for example, it is OK to replace b with a constant array in a[b[0]].

Definition at line 123 of file replace_symbol.h.

Member Function Documentation

◆ replace()

bool address_of_aware_replace_symbolt::replace ( exprt & dest) const
overridevirtual

Reimplemented from replace_symbolt.

Definition at line 352 of file replace_symbol.cpp.

◆ replace_symbol_expr()

bool address_of_aware_replace_symbolt::replace_symbol_expr ( symbol_exprt & dest) const
overrideprivatevirtual

Reimplemented from replace_symbolt.

Definition at line 416 of file replace_symbol.cpp.

Member Data Documentation

◆ require_lvalue

bool address_of_aware_replace_symbolt::require_lvalue = false
mutableprivate

Definition at line 129 of file replace_symbol.h.


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