30 current = index->array();
36 current = member->compound();
41 "Unable to find base object of expression: " +
42 current.get().pretty(1, 0));
100 const exprt &expression,
110 INVARIANT(size,
"Objects are expected to have well defined size");
113 object.unique_id = object_map.size();
121 const exprt &expression,
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A constant literal expression.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
exprt make_invalid_pointer_expr()
Create the invalid pointer constant.
exprt find_object_base_expression(const address_of_exprt &address_of)
The model of addresses we use consists of a unique object identifier and an offset.
void track_expression_objects(const exprt &expression, const namespacet &ns, smt_object_mapt &object_map)
Finds all the object expressions in the given expression and adds them to the object map for cases wh...
bool objects_are_already_tracked(const exprt &expression, const smt_object_mapt &object_map)
Finds whether all base object expressions in the given expression are already tracked in the given ob...
static decision_procedure_objectt make_invalid_pointer_object()
smt_object_mapt initial_smt_object_map()
Constructs an initial object map containing the null object.
static decision_procedure_objectt make_null_object()
static bool is_dynamic(const exprt &object)
This function returns true for heap allocated objects or false for stack allocated objects.
Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the o...
void find_object_base_expressions(const exprt &expression, const output_object_functiont &output_object)
Arbitrary expressions passed to the decision procedure may have multiple address of operations as its...
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
Information the decision procedure holds about each object.
exprt base_expression
The expression for the root of the object.