CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
object_tracking.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
30
31#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
32#define CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
33
34#include <util/expr.h>
35#include <util/pointer_expr.h>
36
37#include <unordered_map>
38
52
59
75template <typename output_object_functiont>
77 const exprt &expression,
78 const output_object_functiont &output_object)
79{
80 expression.visit_pre([&](const exprt &node) {
82 {
84 }
85 });
86}
87
91 std::unordered_map<exprt, decision_procedure_objectt, irep_hash>;
92
97
108 const exprt &expression,
109 const namespacet &ns,
110 smt_object_mapt &object_map);
111
117 const exprt &expression,
118 const smt_object_mapt &object_map);
119
122
123#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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...
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.
smt_object_mapt initial_smt_object_map()
Constructs an initial object map containing the null object.
API to expression classes for Pointers.
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.