CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
constant_pointer_abstract_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_CONSTANT_POINTER_ABSTRACT_OBJECT_H
12#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H
13
14#include <iosfwd>
15
18
20{
21private:
24
25public:
33
35 const typet &type,
37
43 const exprt &expr,
44 const abstract_environmentt &environment,
45 const namespacet &ns);
46
56 exprt to_constant() const override;
57
66 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
67 const override;
68
80 const namespacet &ns) const override;
81
100 abstract_environmentt &environment,
101 const namespacet &ns,
102 const std::stack<exprt> &stack,
103 const abstract_object_pointert &value,
104 bool merging_write) const override;
105
107 const typet &new_type,
108 const abstract_environmentt &environment,
109 const namespacet &ns) const override;
110
112 const exprt &expr,
113 const std::vector<abstract_object_pointert> &operands,
114 const abstract_environmentt &environment,
115 const namespacet &ns) const override;
116
118 const exprt &expr,
119 const std::vector<abstract_object_pointert> &operands,
120 const abstract_environmentt &environment,
121 const namespacet &ns) const override;
122
123 void get_statistics(
124 abstract_object_statisticst &statistics,
127 const namespacet &ns) const override;
128
129protected:
140 const abstract_object_pointert &op1,
141 const widen_modet &widen_mode) const override;
142
144
145 exprt to_predicate_internal(const exprt &name) const override;
146
147private:
148 bool same_target(abstract_object_pointert other) const;
149 exprt offset() const;
151
163 const widen_modet &widen_mode) const;
164
166};
167
168#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H // NOLINT(*)
#define CLONE
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
The base of all pointer abstractions.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
abstract_object_pointert merge(const abstract_object_pointert &op1, const widen_modet &widen_mode) const override
Set this abstract object to be the result of merging this abstract object.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other, const widen_modet &widen_mode) const
Merges two constant pointers.
bool same_target(abstract_object_pointert other) const
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt offset_from(abstract_object_pointert other) const
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
exprt to_constant() const override
To try and find a constant expression for this abstract object.
abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const override
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 override
A helper function to evaluate writing to a pointers value.
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
Represents a stack of write operations to an addressable memory location.