cprover
|
#include <replace_symbol.h>
Public Types | |
typedef std::unordered_map< irep_idt, exprt, irep_id_hash > | expr_mapt |
typedef std::unordered_map< irep_idt, typet, irep_id_hash > | 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 |
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 20 of file replace_symbol.h.
typedef std::unordered_map<irep_idt, exprt, irep_id_hash> replace_symbolt::expr_mapt |
Definition at line 23 of file replace_symbol.h.
typedef std::unordered_map<irep_idt, typet, irep_id_hash> replace_symbolt::type_mapt |
Definition at line 24 of file replace_symbol.h.
replace_symbolt::replace_symbolt | ( | ) |
Definition at line 14 of file replace_symbol.cpp.
Referenced by empty().
|
virtual |
Definition at line 18 of file replace_symbol.cpp.
References expr_map, symbol_exprt::get_identifier(), and insert().
Referenced by empty().
|
inline |
Definition at line 54 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 60 of file replace_symbol.h.
References expr_map, replace_symbolt(), type_map, and ~replace_symbolt().
|
protected |
Definition at line 76 of file replace_symbol.cpp.
References expr_map, irept::find(), forall_operands, irept::get(), irept::id(), irept::is_not_nil(), and exprt::type().
Referenced by have_to_replace(), replace_symbol_extt::replace(), and replace().
|
protected |
Definition at line 168 of file replace_symbol.cpp.
References struct_union_typet::components(), forall_subtypes, irept::get(), 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(), and type_map.
Definition at line 26 of file replace_symbol.h.
References expr_map.
Referenced by code_contractst::add_contract_check(), code_contractst::apply_contract(), linkingt::duplicate_object_symbol(), concurrency_instrumentationt::instrument(), model_argc_argv(), unpack_rec(), and ~replace_symbolt().
void replace_symbolt::insert | ( | const class symbol_exprt & | old_expr, |
const exprt & | new_expr | ||
) |
Definition at line 35 of file replace_symbol.h.
|
inline |
Definition at line 44 of file replace_symbol.h.
References replace().
|
inline |
Definition at line 49 of file replace_symbol.h.
References replace().
|
virtual |
Reimplemented in replace_symbol_extt.
Definition at line 30 of file replace_symbol.cpp.
References irept::add(), expr_map, irept::find(), Forall_operands, irept::get(), have_to_replace(), irept::id(), irept::is_not_nil(), and exprt::type().
Referenced by insert(), operator()(), replace_symbol_extt::replace(), and replace().
|
virtual |
Definition at line 107 of file replace_symbol.cpp.
References struct_union_typet::components(), Forall_subtypes, irept::get(), 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(), and type_map.
expr_mapt replace_symbolt::expr_map |
Definition at line 68 of file replace_symbol.h.
Referenced by clear(), empty(), have_to_replace(), insert(), link_functions(), constant_propagator_domaint::valuest::meet(), constant_propagator_domaint::valuest::merge(), replace_symbol_extt::replace(), replace(), constant_propagator_domaint::valuest::set_to(), and ~replace_symbolt().
type_mapt replace_symbolt::type_map |
Definition at line 69 of file replace_symbol.h.
Referenced by clear(), empty(), have_to_replace(), insert(), and replace().