26 const exprt &new_expr)
30 "types to be replaced should match. old type:\n" +
32 expr_map.insert(std::pair<irep_idt, exprt>(
51 s.
type() == it->second.type(),
52 "types to be replaced should match. s.type:\n" + s.
type().
pretty() +
53 "\nit->second.type:\n" + it->second.type().pretty());
55 static_cast<exprt &
>(s) = it->second;
70 const exprt &const_dest(dest);
80 if(dest.
id()==ID_member)
87 else if(dest.
id()==ID_index)
97 else if(dest.
id()==ID_address_of)
104 else if(dest.
id()==ID_symbol)
109 else if(dest.
id() == ID_let)
114 for(
auto &op : let_expr.values())
120 for(
auto &variable : let_expr.variables())
121 bindings.insert(variable.get_identifier());
130 dest.
id() == ID_array_comprehension || dest.
id() == ID_exists ||
131 dest.
id() == ID_forall || dest.
id() == ID_lambda)
136 for(
auto &binding : binding_expr.variables())
137 bindings.insert(binding.get_identifier());
139 if(!
replace(binding_expr.where()))
151 const typet &c_sizeof_type =
152 static_cast<const typet&
>(dest.
find(ID_C_c_sizeof_type));
156 const typet &va_arg_type =
157 static_cast<const typet&
>(dest.
find(ID_C_va_arg_type));
176 if(dest.
id()==ID_symbol)
185 for(
const auto &op : dest.
operands())
191 const irept &c_sizeof_type=dest.
find(ID_C_c_sizeof_type);
197 const irept &va_arg_type=dest.
find(ID_C_va_arg_type);
223 if(dest.
id()==ID_struct ||
232 else if(dest.
id()==ID_code)
242 const exprt &spec_assigns =
243 static_cast<const exprt &
>(dest.
find(ID_C_spec_assigns));
247 const exprt &spec_frees =
248 static_cast<const exprt &
>(dest.
find(ID_C_spec_frees));
252 const exprt &spec_ensures =
253 static_cast<const exprt &
>(dest.
find(ID_C_spec_ensures));
257 const exprt &spec_requires =
258 static_cast<const exprt &
>(dest.
find(ID_C_spec_requires));
262 else if(dest.
id()==ID_array)
287 if(dest.
id()==ID_struct ||
293 for(
const auto &c : struct_union_type.
components())
297 else if(dest.
id()==ID_code)
307 const exprt &spec_assigns =
308 static_cast<const exprt &
>(dest.
find(ID_C_spec_assigns));
312 const exprt &spec_ensures =
313 static_cast<const exprt &
>(dest.
find(ID_C_spec_ensures));
317 const exprt &spec_requires =
318 static_cast<const exprt &
>(dest.
find(ID_C_spec_requires));
322 else if(dest.
id()==ID_array)
330 const exprt &new_expr)
343 static_cast<exprt &
>(s) = it->second;
354 const exprt &const_dest(dest);
373 if(dest.
id() == ID_index)
385 else if(dest.
id() == ID_address_of)
401 const typet &c_sizeof_type =
402 static_cast<const typet &
>(dest.
find(ID_C_c_sizeof_type));
405 static_cast<typet &
>(dest.
add(ID_C_c_sizeof_type)));
407 const typet &va_arg_type =
408 static_cast<const typet &
>(dest.
find(ID_C_va_arg_type));
411 static_cast<typet &
>(dest.
add(ID_C_va_arg_type)));
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
Operator to return the address of an object.
const exprt & size() const
const typet & return_type() const
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & id() const
irept & add(const irep_idt &name)
Extract member of struct or union.
const exprt & struct_op() const
virtual bool replace(exprt &dest) const
bool have_to_replace(const exprt &dest) const
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
std::set< irep_idt > bindings
virtual ~replace_symbolt()
virtual bool replace_symbol_expr(symbol_exprt &dest) const
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 nothi...
bool replaces_symbol(const irep_idt &id) const
Base type for structs and unions.
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The type of an expression, extends irept.
bool replace_symbol_expr(symbol_exprt &dest) const override
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
#define Forall_operands(it, expr)
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Deprecated expression utility functions.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)