40 "unexpected assignment to member of '" + type.
id_string() +
"'");
77 if_true.add_source_location() = source_location;
80 if_false.add_source_location() = source_location;
94 deref.add_source_location() = source_location;
116 "no function pointer calls in loop assigns clause targets");
123 "can only handle built-in function calls in assigns clause targets");
135 std::unordered_set<exprt, irep_hash> result;
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Operator to dereference a pointer.
Base class for all expressions.
const source_locationt & source_location() const
const std::string & id_string() const
const irep_idt & id() const
The type of an expression, extends irept.
static exprt slice_op_to_deref(const exprt &expr)
Translates object slice expressions found in assigns clause targets to dereference expressions so tha...
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.
static void root_objects_rec(const exprt &expr, std::unordered_set< exprt, irep_hash > &dest)
Recursively computes a set of root object expressions for expr.
Utility functions that compute root object expressions for assigns clause targets and LHS expressions...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
API to expression classes for Pointers.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.