cprover
Loading...
Searching...
No Matches
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:
28
36
38 const typet &type,
40
46 const exprt &expr,
47 const abstract_environmentt &environment,
48 const namespacet &ns);
49
59 exprt to_constant() const override;
60
69 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
70 const override;
71
83 const namespacet &ns) const override;
84
103 abstract_environmentt &environment,
104 const namespacet &ns,
105 const std::stack<exprt> &stack,
106 const abstract_object_pointert &value,
107 bool merging_write) const override;
108
110 const typet &new_type,
111 const abstract_environmentt &environment,
112 const namespacet &ns) const override;
113
115 const exprt &expr,
116 const std::vector<abstract_object_pointert> &operands,
117 const abstract_environmentt &environment,
118 const namespacet &ns) const override;
119
121 const exprt &expr,
122 const std::vector<abstract_object_pointert> &operands,
123 const abstract_environmentt &environment,
124 const namespacet &ns) const override;
125
126 void get_statistics(
127 abstract_object_statisticst &statistics,
130 const namespacet &ns) const override;
131
132protected:
143 const abstract_object_pointert &op1,
144 const widen_modet &widen_mode) const override;
145
146 CLONE
147
148 exprt to_predicate_internal(const exprt &name) const override;
149
150private:
151 bool same_target(abstract_object_pointert other) const;
152 exprt offset() const;
154
166 const widen_modet &widen_mode) const;
167
169};
170
171#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:119
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
CLONE 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:54
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.