17 const auto &state =
ok_expr.state();
18 const auto &pointer =
ok_expr.address();
19 const auto &size =
ok_expr.size();
signedbv_typet signed_size_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The plus expression Associativity is not specified.
The offset (in bytes) of a pointer relative to the object.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
Fixed-width bit-vector with unsigned binary interpretation.
exprt flatten(const state_ok_exprt &ok_expr)
exprt object_size(const exprt &pointer)
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.