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
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
std::set< goto_programt::const_targett > locationst
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
const typet & type() const override
Get the real type of the variable this abstract object is representing.
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:92
The type of an expression, extends irept.
Definition: type.h:28
abstract_object_pointert visit(const abstract_object_pointert element) const
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
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...
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...
abstract_objectt::locationst last_written_locations
write_location_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
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.
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.
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.
virtual abstract_objectt::locationst get_last_written_locations() const
void set_last_written_locations(const abstract_objectt::locationst &locations)
Sets the last written locations for this context.
write_location_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
write_location_contextt(const abstract_object_pointert child, const typet &type)
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.
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...
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...
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...