cprover
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 {
23 public:
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)
30  {
31  child_abstract_object = child;
32  }
33 
35  const abstract_object_pointert child,
36  const typet &type,
37  bool top,
38  bool bottom)
40  {
41  child_abstract_object = child;
42  }
43 
45  const abstract_object_pointert child,
46  const exprt &expr,
47  const abstract_environmentt &environment,
48  const namespacet &ns)
49  : abstract_objectt(expr, environment, ns)
50  {
51  child_abstract_object = child;
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 
84  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
85  const override;
86 
88 
89  void get_statistics(
90  abstract_object_statisticst &statistics,
91  abstract_object_visitedt &visited,
92  const abstract_environmentt &env,
93  const namespacet &ns) const override;
94 
96 
97 protected:
98  CLONE
99 
100  // The abstract_objectt that will be wrapped in a context
102 
103  void set_child(const abstract_object_pointert &child);
104 
105  // These are internal hooks that allow sub-classes to perform additional
106  // actions when an abstract_object is set/unset to TOP
107  void set_top_internal() override;
108  void set_not_top_internal() override;
109 
111  abstract_environmentt &environment,
112  const namespacet &ns,
113  const std::stack<exprt> &stack,
114  const exprt &specifier,
115  const abstract_object_pointert &value,
116  bool merging_write) const override;
117 
118  bool has_been_modified(const abstract_object_pointert before) const override;
119 };
120 
121 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H
context_abstract_objectt::expression_transform
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.
Definition: context_abstract_object.cpp:86
context_abstract_objectt::set_top_internal
void set_top_internal() override
Definition: context_abstract_object.cpp:21
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
context_abstract_objectt::context_abstract_objectt
context_abstract_objectt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Definition: context_abstract_object.h:44
context_abstract_objectt::output
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.
Definition: context_abstract_object.cpp:119
typet
The type of an expression, extends irept.
Definition: type.h:28
context_abstract_objectt::context_abstract_objectt
context_abstract_objectt(const abstract_object_pointert child, const typet &type)
Definition: context_abstract_object.h:26
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
context_abstract_objectt::get_child
abstract_object_pointert get_child() const
Definition: context_abstract_object.cpp:11
context_abstract_objectt::unwrap_context
abstract_object_pointert unwrap_context() const override
Definition: context_abstract_object.cpp:148
CLONE
#define CLONE
Definition: abstract_object.h:47
abstract_object.h
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
context_abstract_objectt::is_top
bool is_top() const override
Find out if the abstract object is top.
Definition: context_abstract_object.h:63
context_abstract_objectt::write
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.
Definition: context_abstract_object.cpp:49
context_abstract_objectt::set_not_top_internal
void set_not_top_internal() override
Definition: context_abstract_object.cpp:27
context_abstract_objectt::child_abstract_object
CLONE abstract_object_pointert child_abstract_object
Definition: context_abstract_object.h:101
context_abstract_objectt::type
const typet & type() const override
Get the real type of the variable this abstract object is representing.
Definition: context_abstract_object.h:58
context_abstract_objectt
Definition: context_abstract_object.h:22
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
context_abstract_objectt::has_been_modified
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...
Definition: context_abstract_object.cpp:135
context_abstract_objectt::~context_abstract_objectt
virtual ~context_abstract_objectt()
Definition: context_abstract_object.h:54
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
context_abstract_objectt::is_bottom
bool is_bottom() const override
Find out if the abstract object is bottom.
Definition: context_abstract_object.h:68
context_abstract_objectt::context_abstract_objectt
context_abstract_objectt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
Definition: context_abstract_object.h:34
abstract_objectt::top
bool top
Definition: abstract_object.h:363
context_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: context_abstract_object.cpp:153
abstract_objectt
Definition: abstract_object.h:79
context_abstract_objectt::set_child
void set_child(const abstract_object_pointert &child)
Definition: context_abstract_object.cpp:16
context_abstract_objectt::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: context_abstract_object.h:73