cprover
|
#include <replace_symbol.h>
Public Types | |
typedef std::unordered_map< irep_idt, exprt > | expr_mapt |
typedef std::unordered_map< irep_idt, typet > | type_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 |
Definition at line 22 of file replace_symbol.h.
typedef std::unordered_map<irep_idt, exprt> replace_symbolt::expr_mapt |
Definition at line 25 of file replace_symbol.h.
typedef std::unordered_map<irep_idt, typet> replace_symbolt::type_mapt |
Definition at line 26 of file replace_symbol.h.
replace_symbolt::replace_symbolt | ( | ) |
Definition at line 14 of file replace_symbol.cpp.
|
virtual |
Definition at line 18 of file replace_symbol.cpp.
|
inline |
Definition at line 71 of file replace_symbol.h.
References expr_map, and type_map.
Referenced by constant_propagator_domaint::valuest::set_to_bottom(), and constant_propagator_domaint::valuest::set_to_top().
|
inline |
Definition at line 77 of file replace_symbol.h.
References expr_map, and type_map.
Referenced by constant_propagator_domaint::valuest::is_bot(), and constant_propagator_domaint::valuest::is_top().
|
protected |
Definition at line 111 of file replace_symbol.cpp.
References expr_map, irept::find(), forall_operands, symbol_exprt::get_identifier(), irept::id(), irept::is_not_nil(), to_symbol_expr(), exprt::type(), and type_map.
Referenced by have_to_replace(), and replace().
|
protected |
Definition at line 210 of file replace_symbol.cpp.
References struct_union_typet::components(), expr_map, forall_subtypes, symbol_typet::get_identifier(), typet::has_subtype(), have_to_replace(), irept::id(), code_typet::parameters(), code_typet::return_type(), array_typet::size(), typet::subtype(), to_array_type(), to_code_type(), to_struct_union_type(), to_symbol_type(), and type_map.
Definition at line 28 of file replace_symbol.h.
References expr_map.
Referenced by actuals_replace_map(), code_contractst::add_contract_check(), code_contractst::apply_contract(), dump_ct::cleanup_harness(), linkingt::duplicate_object_symbol(), concurrency_instrumentationt::instrument(), model_argc_argv(), and unpack_rec().
void replace_symbolt::insert | ( | const class symbol_exprt & | old_expr, |
const exprt & | new_expr | ||
) |
Definition at line 37 of file replace_symbol.h.
References type_map.
|
inline |
Definition at line 61 of file replace_symbol.h.
References replace().
|
inline |
Definition at line 66 of file replace_symbol.h.
References replace().
|
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]].
dest | The expression in which to do the replacement |
replace_with_const | If 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().
|
virtual |
Definition at line 148 of file replace_symbol.cpp.
References struct_union_typet::components(), Forall_subtypes, typet::has_subtype(), have_to_replace(), irept::id(), code_typet::parameters(), replace(), code_typet::return_type(), array_typet::size(), typet::subtype(), to_array_type(), to_code_type(), to_struct_union_type(), to_symbol_type(), and type_map.
expr_mapt replace_symbolt::expr_map |
Definition at line 85 of file replace_symbol.h.
Referenced by clear(), empty(), have_to_replace(), insert(), constant_propagator_domaint::valuest::is_constant(), constant_propagator_domaint::valuest::is_empty(), link_functions(), constant_propagator_domaint::valuest::meet(), constant_propagator_domaint::valuest::merge(), replace(), and constant_propagator_domaint::valuest::set_to().
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().