cprover
Loading...
Searching...
No Matches
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:
25 explicit abstract_pointer_objectt(const typet &type);
26
33 abstract_pointer_objectt(const typet &type, bool top, bool bottom);
34
41 const exprt &expr,
42 const abstract_environmentt &environment,
43 const namespacet &ns);
44
46 const exprt &expr,
47 const std::vector<abstract_object_pointert> &operands,
48 const abstract_environmentt &environment,
49 const namespacet &ns) const override;
50
52 abstract_environmentt &environment,
53 const namespacet &ns,
54 const std::stack<exprt> &stack,
55 const exprt &specifier,
56 const abstract_object_pointert &value,
57 bool merging_write) const override;
58
59 void get_statistics(
62 const abstract_environmentt &env,
63 const namespacet &ns) const override;
64
73 const abstract_environmentt &env,
74 const namespacet &ns) const = 0;
75
93 abstract_environmentt &environment,
94 const namespacet &ns,
95 const std::stack<exprt> &stack,
96 const abstract_object_pointert &value,
97 bool merging_write) const = 0;
98
100 const typet &new_type,
101 const abstract_environmentt &environment,
102 const namespacet &ns) const = 0;
103
105 const exprt &expr,
106 const std::vector<abstract_object_pointert> &operands,
107 const abstract_environmentt &environment,
108 const namespacet &ns) const = 0;
109
111 const exprt &expr,
112 const std::vector<abstract_object_pointert> &operands,
113 const abstract_environmentt &environment,
114 const namespacet &ns) const = 0;
115
116private:
118 const exprt &expr,
119 const std::vector<abstract_object_pointert> &operands,
120 const abstract_environmentt &environment,
121 const namespacet &ns) const;
123 const exprt &expr,
124 const std::vector<abstract_object_pointert> &operands,
125 const abstract_environmentt &environment,
126 const namespacet &ns) const;
128 const exprt &expr,
129 const std::vector<abstract_object_pointert> &operands,
130 const abstract_environmentt &environment,
131 const namespacet &ns) const;
132};
133
134#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
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