cprover
replace_symbolt Class Reference

#include <replace_symbol.h>

Collaboration diagram for replace_symbolt:
[legend]

Public Types

typedef std::unordered_map< irep_idt, exprtexpr_mapt
 
typedef std::unordered_map< irep_idt, typettype_mapt
 

Public Member Functions

void insert (const irep_idt &identifier, const exprt &expr)
 
void insert (const class symbol_exprt &old_expr, const exprt &new_expr)
 
void insert (const irep_idt &identifier, const typet &type)
 
virtual bool replace (exprt &dest, const bool replace_with_const=true) const
 Replaces a symbol with a constant If you are replacing symbols with constants in an l-value, you can create something that is not an l-value. More...
 
virtual bool replace (typet &dest) const
 
void operator() (exprt &dest) const
 
void operator() (typet &dest) const
 
void clear ()
 
bool empty () const
 
 replace_symbolt ()
 
virtual ~replace_symbolt ()
 

Public Attributes

expr_mapt expr_map
 
type_mapt type_map
 

Protected Member Functions

bool have_to_replace (const exprt &dest) const
 
bool have_to_replace (const typet &type) const
 

Detailed Description

Definition at line 22 of file replace_symbol.h.

Member Typedef Documentation

◆ expr_mapt

typedef std::unordered_map<irep_idt, exprt> replace_symbolt::expr_mapt

Definition at line 25 of file replace_symbol.h.

◆ type_mapt

typedef std::unordered_map<irep_idt, typet> replace_symbolt::type_mapt

Definition at line 26 of file replace_symbol.h.

Constructor & Destructor Documentation

◆ replace_symbolt()

replace_symbolt::replace_symbolt ( )

Definition at line 14 of file replace_symbol.cpp.

◆ ~replace_symbolt()

replace_symbolt::~replace_symbolt ( )
virtual

Definition at line 18 of file replace_symbol.cpp.

Member Function Documentation

◆ clear()

void replace_symbolt::clear ( void  )
inline

◆ empty()

bool replace_symbolt::empty ( ) const
inline

◆ have_to_replace() [1/2]

bool replace_symbolt::have_to_replace ( const exprt dest) const
protected

◆ have_to_replace() [2/2]

◆ insert() [1/3]

◆ insert() [2/3]

void replace_symbolt::insert ( const class symbol_exprt old_expr,
const exprt new_expr 
)

◆ insert() [3/3]

void replace_symbolt::insert ( const irep_idt identifier,
const typet type 
)
inline

Definition at line 37 of file replace_symbol.h.

References type_map.

◆ operator()() [1/2]

void replace_symbolt::operator() ( exprt dest) const
inline

Definition at line 61 of file replace_symbol.h.

References replace().

◆ operator()() [2/2]

void replace_symbolt::operator() ( typet dest) const
inline

Definition at line 66 of file replace_symbol.h.

References replace().

◆ replace() [1/2]

bool replace_symbolt::replace ( exprt dest,
const bool  replace_with_const = true 
) const
virtual

Replaces a symbol with a constant 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]].

Parameters
destThe expression in which to do the replacement
replace_with_constIf false then it disables the rewrites that could result in something that is not an l-value.

Definition at line 30 of file replace_symbol.cpp.

References irept::add(), index_exprt::array(), expr_map, irept::find(), Forall_operands, symbol_exprt::get_identifier(), have_to_replace(), irept::id(), index_exprt::index(), exprt::is_constant(), irept::is_not_nil(), address_of_exprt::object(), member_exprt::struct_op(), to_address_of_expr(), to_index_expr(), to_member_expr(), to_symbol_expr(), and exprt::type().

Referenced by operator()(), replace(), and constant_propagator_domaint::replace_constants_and_simplify().

◆ replace() [2/2]

Member Data Documentation

◆ expr_map

◆ type_map

type_mapt replace_symbolt::type_map

Definition at line 86 of file replace_symbol.h.

Referenced by clear(), empty(), have_to_replace(), insert(), and replace().


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