163 const exprt *p = &expr;
202 "dereference expression's operand must have a pointer type");
207 "dereference expression's type must match the base type of the type of its "
void base_type(typet &type, const namespacet &ns)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
address_of_exprt(const exprt &op)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for binary expressions.
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
unsigned int get_instance() const
void set_instance(unsigned int instance)
element_address_exprt(exprt base, exprt index)
constructor for element addresses.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & component_name() const
const typet & compound_type() const
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
void set(const irep_idt &name, const irep_idt &value)
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...
An expression without operands.
const pointer_typet & type() const
symbol_exprt object_expr() const
irep_idt object_identifier() const
object_address_exprt(const symbol_exprt &)
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 ...
const typet & base_type() const
The type of the data what we point to.
Expression to hold a symbol (variable)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...