cprover
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 {
21 private:
24 
25 public:
28 
36 
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 
82  const abstract_environmentt &env,
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 
109  void get_statistics(
110  abstract_object_statisticst &statistics,
111  abstract_object_visitedt &visited,
112  const abstract_environmentt &env,
113  const namespacet &ns) const override;
114 
115 protected:
125 
126  CLONE
127 
128 private:
138  const constant_pointer_abstract_pointert &other) const;
139 
141 };
142 
143 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H // NOLINT(*)
constant_pointer_abstract_objectt::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
Definition: constant_pointer_abstract_object.cpp:113
write_stack.h
Represents a stack of write operations to an addressable memory location.
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
constant_pointer_abstract_objectt::merge_constant_pointers
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other) const
Merges two constant pointers.
Definition: constant_pointer_abstract_object.cpp:76
constant_pointer_abstract_objectt::merge
abstract_object_pointert merge(abstract_object_pointert op1) const override
Set this abstract object to be the result of merging this abstract object.
Definition: constant_pointer_abstract_object.cpp:60
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
constant_pointer_abstract_objectt::write_dereference
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.
Definition: constant_pointer_abstract_object.cpp:174
constant_pointer_abstract_objectt::value_stack
write_stackt value_stack
Definition: constant_pointer_abstract_object.h:140
abstract_pointer_objectt
Definition: abstract_pointer_object.h:22
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
sharing_ptrt
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
Definition: abstract_object.h:73
CLONE
#define CLONE
Definition: abstract_object.h:47
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
constant_pointer_abstract_objectt::constant_pointer_abstract_pointert
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
Definition: constant_pointer_abstract_object.h:23
write_stackt
Definition: write_stack.h:19
constant_pointer_abstract_objectt::read_dereference
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
Definition: constant_pointer_abstract_object.cpp:156
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
constant_pointer_abstract_objectt
Definition: constant_pointer_abstract_object.h:20
constant_pointer_abstract_objectt::to_constant
exprt to_constant() const override
To try and find a constant expression for this abstract object.
Definition: constant_pointer_abstract_object.cpp:99
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
constant_pointer_abstract_objectt(const typet &type)
Definition: constant_pointer_abstract_object.cpp:19
abstract_pointer_object.h
The base of all pointer abstractions.
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
constant_pointer_abstract_objectt::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: constant_pointer_abstract_object.cpp:222
abstract_objectt::top
bool top
Definition: abstract_object.h:363