cprover
Loading...
Searching...
No Matches
context_abstract_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity context_abstract_object
4
5 Author: Diffblue Ltd
6
7\*******************************************************************/
8#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H
9#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H
10
12
22{
23public:
24 // These constructors mirror those in the base abstract_objectt, but with
25 // the addition of an extra argument which is the abstract_objectt to wrap.
33
43
46 const exprt &expr,
47 const abstract_environmentt &environment,
48 const namespacet &ns)
49 : abstract_objectt(expr, environment, ns)
50 {
52 }
53
55 {
56 }
57
58 const typet &type() const override
59 {
60 return child_abstract_object->type();
61 }
62
63 bool is_top() const override
64 {
65 return child_abstract_object->is_top();
66 }
67
68 bool is_bottom() const override
69 {
70 return child_abstract_object->is_bottom();
71 }
72
73 exprt to_constant() const override
74 {
75 return child_abstract_object->to_constant();
76 }
77
79 const exprt &expr,
80 const std::vector<abstract_object_pointert> &operands,
81 const abstract_environmentt &environment,
82 const namespacet &ns) const override;
83
93 write_location_context(const locationt &location) const override;
94
95 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
96 const override;
97
100
101 void get_statistics(
102 abstract_object_statisticst &statistics,
105 const namespacet &ns) const override;
106
108
109protected:
111 std::shared_ptr<context_abstract_objectt>;
112
113 // The abstract_objectt that will be wrapped in a context
115
117
118 // These are internal hooks that allow sub-classes to perform additional
119 // actions when an abstract_object is set/unset to TOP
120 void set_top_internal() override;
121 void set_not_top_internal() override;
122
124 abstract_environmentt &environment,
125 const namespacet &ns,
126 const std::stack<exprt> &stack,
127 const exprt &specifier,
128 const abstract_object_pointert &value,
129 bool merging_write) const override;
130
131 bool has_been_modified(const abstract_object_pointert &before) const override;
132
133 exprt to_predicate_internal(const exprt &name) const override;
134
135 typedef std::set<locationt> locationst;
136
139};
140
141#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_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
goto_programt::const_targett locationt
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
bool is_bottom() const override
Find out if the abstract object is bottom.
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
virtual context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const =0
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
abstract_object_pointert envelop(abstract_object_pointert &child) const
context_abstract_objectt(const abstract_object_pointert child, const typet &type)
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Output a representation of the value of this abstract object.
bool has_been_modified(const abstract_object_pointert &before) const override
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
context_abstract_objectt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
context_abstract_objectt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert child_abstract_object
void set_child(const abstract_object_pointert &child)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Try to resolve an expression with the maximum level of precision available.
bool is_top() const override
Find out if the abstract object is top.
exprt to_constant() const override
Converts to a constant expression if possible.
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.
abstract_object_pointert get_child() const
const typet & type() const override
Get the real type of the variable this abstract object is representing.
abstract_object_pointert unwrap_context() const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
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