17 const auto &state =
ok_expr.state();
18 const auto &pointer =
ok_expr.address();
19 const auto &size =
ok_expr.size();
unsignedbv_typet size_type()
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.
std::size_t get_width() const
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(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...