cprover
write_location_context.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity write_location_context
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
16 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
17 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
18 
20 #include <iostream>
21 #include <stack>
22 
35 {
36 public:
38  const abstract_object_pointert child,
39  const typet &type)
41  {
42  }
43 
45  const abstract_object_pointert child,
46  const typet &type,
47  bool top,
48  bool bottom)
50  {
51  }
52 
54  const abstract_object_pointert child,
55  const exprt &expr,
56  const abstract_environmentt &environment,
57  const namespacet &ns)
58  : context_abstract_objectt(child, expr, environment, ns)
59  {
60  }
61 
63  {
64  }
65 
66  // Standard abstract_objectt interface
67 
68  bool has_been_modified(const abstract_object_pointert before) const override;
69 
71  const abstract_objectt::locationst &locations,
72  const bool update_sub_elements) const override;
73 
74  // A visitor class to update the last_written_locations of any visited
75  // abstract_object with a given set of locations.
78  {
79  public:
82  {
83  }
84 
86  {
87  return element->update_location_context(locations, true);
88  }
89 
90  private:
92  };
93 
94  locationst get_location_union(const locationst &locations) const;
95 
96  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
97  const override;
98 
99 protected:
100  CLONE
101 
103 
105  const abstract_object_pointert other) const override;
106 
108  abstract_environmentt &environment,
109  const namespacet &ns,
110  const std::stack<exprt> &stack,
111  const exprt &specifier,
112  const abstract_object_pointert &value,
113  bool merging_write) const override;
114 
115  static void output_last_written_locations(
116  std::ostream &out,
117  const abstract_objectt::locationst &locations);
118 
120 
121 private:
122  // To enforce copy-on-write these are private and have read-only accessors
124 
125  void
127 };
128 
129 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
write_location_contextt::write_location_contextt
write_location_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Definition: write_location_context.h:53
write_location_contextt::get_location_union
locationst get_location_union(const locationst &locations) const
Construct the union of the location set of the current object, and a the provided location set.
Definition: write_location_context.cpp:228
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
typet
The type of an expression, extends irept.
Definition: type.h:28
write_location_contextt::location_update_visitort::location_update_visitort
location_update_visitort(const locationst &locations)
Definition: write_location_context.h:80
context_abstract_object.h
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
write_location_contextt::location_update_visitort::locations
const locationst & locations
Definition: write_location_context.h:91
write_location_contextt::location_update_visitort
Definition: write_location_context.h:78
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
CLONE
#define CLONE
Definition: abstract_object.h:47
write_location_contextt::last_written_locations
abstract_objectt::locationst last_written_locations
Definition: write_location_context.h:123
write_location_contextt::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: write_location_context.cpp:246
write_location_contextt::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: write_location_context.cpp:207
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_objectt::locationst
std::set< goto_programt::const_targett > locationst
Definition: abstract_object.h:215
write_location_contextt::set_last_written_locations
void set_last_written_locations(const abstract_objectt::locationst &locations)
Sets the last written locations for this context.
Definition: write_location_context.cpp:193
write_location_contextt::update_location_context
abstract_object_pointert update_location_context(const abstract_objectt::locationst &locations, const bool update_sub_elements) const override
Update the location context for an abstract object, potentially propagating the update to any childre...
Definition: write_location_context.cpp:27
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
write_location_contextt
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
Definition: write_location_context.h:35
write_location_contextt::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: write_location_context.cpp:69
write_location_contextt::get_last_written_locations
virtual abstract_objectt::locationst get_last_written_locations() const
Definition: write_location_context.cpp:48
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
write_location_contextt::write_location_contextt
write_location_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
Definition: write_location_context.h:44
abstract_objectt::abstract_object_visitort
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
Definition: abstract_object.h:327
write_location_contextt::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
Definition: write_location_context.cpp:113
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
write_location_contextt::~write_location_contextt
virtual ~write_location_contextt()
Definition: write_location_context.h:62
write_location_contextt::location_update_visitort::visit
abstract_object_pointert visit(const abstract_object_pointert element) const
Definition: write_location_context.h:85
abstract_objectt::top
bool top
Definition: abstract_object.h:363
write_location_contextt::write_location_contextt
write_location_contextt(const abstract_object_pointert child, const typet &type)
Definition: write_location_context.h:37
write_location_contextt::output_last_written_locations
static void output_last_written_locations(std::ostream &out, const abstract_objectt::locationst &locations)
Internal helper function to format and output a given set of locations.
Definition: write_location_context.cpp:325
write_location_contextt::abstract_object_merge_internal
abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const override
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
Definition: write_location_context.cpp:167