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.
27 const abstract_object_pointert child,
28 const typet &type,
29 bool top,
30 bool bottom)
32 {
34 }
35
37 const abstract_object_pointert child,
38 const exprt &expr,
39 const abstract_environmentt &environment,
40 const namespacet &ns)
41 : abstract_objectt(expr, environment, ns)
42 {
44 }
45
47 {
48 }
49
50 const typet &type() const override
51 {
52 return child_abstract_object->type();
53 }
54
55 bool is_top() const override
56 {
57 return child_abstract_object->is_top();
58 }
59
60 bool is_bottom() const override
61 {
62 return child_abstract_object->is_bottom();
63 }
64
65 exprt to_constant() const override
66 {
67 return child_abstract_object->to_constant();
68 }
69
71 const exprt &expr,
72 const std::vector<abstract_object_pointert> &operands,
73 const abstract_environmentt &environment,
74 const namespacet &ns) const override;
75
85 write_location_context(const locationt &location) const override;
86
87 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
88 const override;
89
92
93 void get_statistics(
96 const abstract_environmentt &env,
97 const namespacet &ns) const override;
98
100
101protected:
103 std::shared_ptr<context_abstract_objectt>;
104
105 // The abstract_objectt that will be wrapped in a context
107
108 void set_child(const abstract_object_pointert &child);
109
110 // These are internal hooks that allow sub-classes to perform additional
111 // actions when an abstract_object is set/unset to TOP
112 void set_top_internal() override;
113 void set_not_top_internal() override;
114
116 abstract_environmentt &environment,
117 const namespacet &ns,
118 const std::stack<exprt> &stack,
119 const exprt &specifier,
120 const abstract_object_pointert &value,
121 bool merging_write) const override;
122
123 bool has_been_modified(const abstract_object_pointert &before) const override;
124
125 exprt to_predicate_internal(const exprt &name) const override;
126
127 typedef std::set<locationt, goto_programt::target_less_than> locationst;
128
130 update_location_context_internal(const locationst &locations) const = 0;
131};
132
133#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
abstract_objectt(const typet &type, bool top, bool bottom)
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
bool is_bottom() const override
Find out if the abstract object is bottom.
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.
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
abstract_object_pointert envelop(abstract_object_pointert &child) const
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.
std::set< locationt, goto_programt::target_less_than > locationst
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:56
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