21 auto current = std::ref(address_of.
object());
31 current = index->array();
37 current = member->compound();
42 "Unable to find base object of expression: " +
43 current.get().pretty(1, 0));
67 return invalid_pointer_object;
75 object_map.emplace(std::move(null_object_base), std::move(
null_object));
80 std::move(invalid_pointer_object_base), std::move(invalid_pointer_object));
91 const bool dynamic_type =
object.type().get_bool(ID_C_dynamic);
95 bool symbol_is_dynamic =
98 return symbol_is_dynamic;
102 const exprt &expression,
107 expression, [&](
const exprt &object_base) ->
void {
108 const auto find_result = object_map.find(object_base);
109 if(find_result != object_map.cend())
112 INVARIANT(size,
"Objects are expected to have well defined size");
115 object.unique_id = object_map.size();
118 object_map.emplace_hint(find_result, object_base, std::move(
object));
123 const exprt &expression,
126 bool all_objects_tracked =
true;
128 expression, [&](
const exprt &object_base) ->
void {
129 const auto find_result = object_map.find(object_base);
130 if(find_result != object_map.cend())
132 all_objects_tracked =
false;
134 return all_objects_tracked;
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
A constant literal expression.
Base class for all expressions.
typet & type()
Return the type of the expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
bool has_prefix(const std::string &s, const std::string &prefix)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
const std::string & id2string(const irep_idt &d)
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.
optionalt< 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'.
bool can_cast_expr< code_labelt >(const exprt &base)
API to expression classes.
bool can_cast_expr< constant_exprt >(const exprt &base)
bool can_cast_expr< symbol_exprt >(const exprt &base)
bool can_cast_expr< string_constantt >(const exprt &base)
Information the decision procedure holds about each object.
exprt base_expression
The expression for the root of the object.
bool is_dynamic
This is true for heap allocated objects and false for stack allocated.
std::size_t unique_id
Number which uniquely identifies this particular object.
exprt size
Expression which evaluates to the size of the object in bytes.