CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
liveness_context.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity region_contextt
4
5 Author: Jez Higgins
6
7\*******************************************************************/
8
9#include "liveness_context.h"
10
12{
13 return assign_location.has_value();
14}
15
20
38 abstract_environmentt &environment,
39 const namespacet &ns,
40 const std::stack<exprt> &stack,
41 const exprt &specifier,
42 const abstract_object_pointert &value,
43 bool merging_write) const
44{
45 auto updated = std::dynamic_pointer_cast<const liveness_contextt>(
47 environment, ns, stack, specifier, value, merging_write));
48 if(updated == shared_from_this())
49 return shared_from_this();
50
51 // record the updated write locations
52 auto result =
53 std::dynamic_pointer_cast<liveness_contextt>(updated->mutable_clone());
54 auto value_context =
55 std::dynamic_pointer_cast<const liveness_contextt>(value);
57 result->set_location(value_context->get_location());
58
59 return result;
60}
61
73 const abstract_object_pointert &other,
74 const widen_modet &widen_mode) const
75{
76 auto cast_other = std::dynamic_pointer_cast<const liveness_contextt>(other);
77
78 if(cast_other)
79 {
80 auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
82 return reset_location_on_merge(merged);
83 }
84
86}
87
89 const abstract_object_pointert &other) const
90{
91 auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
93 return reset_location_on_merge(merged);
94}
95
97 const liveness_context_ptrt &merged) const
98{
99 if(merged == shared_from_this())
100 return shared_from_this();
101
102 auto updated =
103 std::dynamic_pointer_cast<liveness_contextt>(merged->mutable_clone());
104 updated->assign_location.reset();
105 return updated;
106}
107
110 const locationst &locations) const
111{
112 auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
113 result->set_last_written_locations(locations);
114 result->set_location(*locations.cbegin());
115 return result;
116}
117
119{
120 assign_location.emplace(location);
121}
122
132 std::ostream &out,
133 const ai_baset &ai,
134 const namespacet &ns) const
135{
137
138 if(has_location())
139 out << " @ [" << get_location()->location_number << "]";
140 else
141 out << " @ [undefined]";
142}
143
146{
147 if(assign_location.has_value())
148 return shared_from_this();
149
150 auto update = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
151 update->assign_location = location;
152 auto updated_child = child_abstract_object->merge_location_context(location);
153 update->set_child(updated_child);
154
155 return update;
156}
sharing_ptrt< class abstract_objectt > abstract_object_pointert
goto_programt::const_targett locationt
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
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 child_abstract_object
std::set< locationt, goto_programt::target_less_than > locationst
Base class for all expressions.
Definition expr.h:56
void set_location(const locationt &location)
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.
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...
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
std::optional< locationt > assign_location
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.
internal_abstract_object_pointert mutable_clone() const override
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
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...
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...
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.
Maintain a context in the variable sensitvity domain that records the liveness region for a given abs...