cprover
liveness_context.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity liveness_contextt
4 
5  Author: Jez Higgins
6 
7 \*******************************************************************/
8 
15 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
16 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
17 
19 #include <iostream>
20 #include <stack>
21 
34 {
35 public:
37  const abstract_object_pointert child,
38  const typet &type)
40  {
41  }
42 
44  const abstract_object_pointert child,
45  const typet &type,
46  bool top,
47  bool bottom)
49  {
50  }
51 
53  const abstract_object_pointert child,
54  const exprt &expr,
55  const abstract_environmentt &environment,
56  const namespacet &ns)
57  : write_location_contextt(child, expr, environment, ns)
58  {
59  }
60 
62  merge_location_context(const locationt &location) const override;
63 
64  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
65  const override;
66 
67  locationt get_location() const;
68 
69 protected:
70  CLONE
71 
73  const abstract_object_pointert &other,
74  const widen_modet &widen_mode) const override;
75 
77  const abstract_object_pointert &other) const override;
78 
80  abstract_environmentt &environment,
81  const namespacet &ns,
82  const std::stack<exprt> &stack,
83  const exprt &specifier,
84  const abstract_object_pointert &value,
85  bool merging_write) const override;
86 
87 private:
88  using liveness_context_ptrt = std::shared_ptr<const liveness_contextt>;
89 
92 
94 
96  update_location_context_internal(const locationst &locations) const override;
97 
98  bool has_location() const;
99 
100  void set_location(const locationt &location);
101 };
102 
103 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
goto_programt::const_targett locationt
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
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
optionalt< locationt > assign_location
void set_location(const locationt &location)
liveness_contextt(const abstract_object_pointert child, const typet &type)
bool has_location() 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.
liveness_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
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...
liveness_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
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.
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::shared_ptr< const liveness_contextt > liveness_context_ptrt
locationt get_location() const
abstract_object_pointert reset_location_on_merge(const liveness_context_ptrt &merged) const
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...
nonstd::optional< T > optionalt
Definition: optional.h:35
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...