cprover
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 {
23 public:
25  explicit abstract_pointer_objectt(const typet &type);
26 
33  abstract_pointer_objectt(const typet &type, bool top, bool bottom);
34 
40  explicit abstract_pointer_objectt(
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(
60  abstract_object_statisticst &statistics,
61  abstract_object_visitedt &visited,
62  const abstract_environmentt &env,
63  const namespacet &ns) const override;
64 
73  const abstract_environmentt &env,
74  const namespacet &ns) const;
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;
98 };
99 
100 #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 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 read_dereference(const abstract_environmentt &env, const namespacet &ns) const
Evaluate reading the pointer's value.
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
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
Evaluate writing to a pointer's value.
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_pointer_objectt(const typet &type)
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:92
The type of an expression, extends irept.
Definition: type.h:28