35 if(expr.
id() == ID_index)
50 else if(expr.
id() == ID_member)
65 expr.
id() == ID_byte_extract_little_endian ||
66 expr.
id() == ID_byte_extract_big_endian)
79 else if(expr.
id() == ID_typecast)
87 else if(
const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
90 if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
92 dest.
object() = address_of->object();
96 else if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
99 if(
const auto deref = expr_try_dynamic_cast<dereference_exprt>(
object))
101 dest.
object() = deref->pointer();
113 if(
offset().
id() == ID_unknown)
131 if(p->
id() == ID_member)
133 else if(p->
id() == ID_index)
158 const typet &type_of_operand = dereference_expr.pointer().type();
161 type_try_dynamic_cast<pointer_typet>(type_of_operand);
166 "dereference expression's operand must have a pointer type");
171 "dereference expression's type must match the subtype of the type of its "
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet index_type()
pointer_typet pointer_type(const typet &subtype)
address_of_exprt(const exprt &op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
unsigned int get_instance() const
void set_instance(unsigned int instance)
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
Extract member of struct or union.
const exprt & compound() const
const exprt & struct_op() const
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Split an expression into a base object and a (byte) offset.
const exprt & root_object() const
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
static void build_object_descriptor_rec(const namespacet &ns, const exprt &expr, object_descriptor_exprt &dest)
Build an object_descriptor_exprt from a given expr.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...