CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
abstract_pointer_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
11#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
12#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
13
15
17{
18};
19
22{
23public:
30 abstract_pointer_objectt(const typet &type, bool top, bool bottom);
31
38 const exprt &expr,
39 const abstract_environmentt &environment,
40 const namespacet &ns);
41
43 const exprt &expr,
44 const std::vector<abstract_object_pointert> &operands,
45 const abstract_environmentt &environment,
46 const namespacet &ns) const override;
47
49 abstract_environmentt &environment,
50 const namespacet &ns,
51 const std::stack<exprt> &stack,
52 const exprt &specifier,
53 const abstract_object_pointert &value,
54 bool merging_write) const override;
55
56 void get_statistics(
60 const namespacet &ns) const override;
61
71 const namespacet &ns) const = 0;
72
90 abstract_environmentt &environment,
91 const namespacet &ns,
92 const std::stack<exprt> &stack,
93 const abstract_object_pointert &value,
94 bool merging_write) const = 0;
95
97 const typet &new_type,
98 const abstract_environmentt &environment,
99 const namespacet &ns) const = 0;
100
102 const exprt &expr,
103 const std::vector<abstract_object_pointert> &operands,
104 const abstract_environmentt &environment,
105 const namespacet &ns) const = 0;
106
108 const exprt &expr,
109 const std::vector<abstract_object_pointert> &operands,
110 const abstract_environmentt &environment,
111 const namespacet &ns) const = 0;
112
113private:
115 const exprt &expr,
116 const std::vector<abstract_object_pointert> &operands,
117 const abstract_environmentt &environment,
118 const namespacet &ns) const;
120 const exprt &expr,
121 const std::vector<abstract_object_pointert> &operands,
122 const abstract_environmentt &environment,
123 const namespacet &ns) const;
125 const exprt &expr,
126 const std::vector<abstract_object_pointert> &operands,
127 const abstract_environmentt &environment,
128 const namespacet &ns) const;
129};
130
131#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
abstract_object_pointert eval_ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
abstract_object_pointert typecast_from_void_ptr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
virtual abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const =0
Evaluate writing to a pointer's value.
virtual exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0
virtual abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const =0
A helper function to read elements from an array.
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
virtual abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0
virtual abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const =0
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
abstract_object_pointert eval_ptr_comparison(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29