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 
70  locationst get_location_union(const locationst &locations) const;
71 
72  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
73  const override;
74 
75 protected:
76  CLONE
77 
79  const abstract_object_pointert &other,
80  const widen_modet &widen_mode) const override;
82  meet(const abstract_object_pointert &other) const override;
83 
85  const abstract_object_pointert &other) const override;
86 
88  abstract_environmentt &environment,
89  const namespacet &ns,
90  const std::stack<exprt> &stack,
91  const exprt &specifier,
92  const abstract_object_pointert &value,
93  bool merging_write) const override;
94 
95  static void
96  output_last_written_locations(std::ostream &out, const locationst &locations);
97 
98  virtual locationst get_last_written_locations() const;
99  void set_last_written_locations(const locationst &locations);
100 
101 private:
103  const abstract_object_pointert &op1,
104  const abstract_object_pointert &op2)>;
106  std::shared_ptr<const write_location_contextt>;
107 
109  combine(const write_location_context_ptrt &other, combine_fn fn) const;
110 
111  // To enforce copy-on-write these are private and have read-only accessors
113 
115  update_location_context_internal(const locationst &locations) const override;
116 };
117 
118 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
std::set< locationt > locationst
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:91
The type of an expression, extends irept.
Definition: type.h:29
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
CLONE abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
std::function< abstract_objectt::combine_result(const abstract_object_pointert &op1, const abstract_object_pointert &op2)> combine_fn
write_location_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
virtual locationst get_last_written_locations() const
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...
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.
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
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.
write_location_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
static void output_last_written_locations(std::ostream &out, const locationst &locations)
Internal helper function to format and output a given set of locations.
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...
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.
write_location_contextt(const abstract_object_pointert child, const typet &type)
void set_last_written_locations(const locationst &locations)
Sets the last written locations for this context.
std::shared_ptr< const write_location_contextt > write_location_context_ptrt
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
abstract_object_pointert combine(const write_location_context_ptrt &other, combine_fn fn) const
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
Clones the first parameter and merges it with the second.