Go to the documentation of this file.
29 const bool update_sub_elements)
const
32 std::dynamic_pointer_cast<write_location_contextt>(
mutable_clone());
34 if(update_sub_elements)
38 ->update_location_context(locations, update_sub_elements)
40 result->set_child(visited_child);
43 result->set_last_written_locations(locations);
72 const std::stack<exprt> &stack,
73 const exprt &specifier,
75 bool merging_write)
const
78 environment, ns, stack, specifier, value, merging_write);
82 return shared_from_this();
87 std::dynamic_pointer_cast<write_location_contextt>(
mutable_clone());
90 result->set_child(updated_child);
92 std::dynamic_pointer_cast<const write_location_contextt>(value);
96 result->set_last_written_locations(
97 value_context->get_last_written_locations());
116 std::dynamic_pointer_cast<const write_location_contextt>(other);
120 bool child_modified =
false;
128 bool merge_locations =
131 if(child_modified || merge_locations)
134 std::dynamic_pointer_cast<write_location_contextt>(
mutable_clone());
137 result->set_child(merged_child);
141 result->set_last_written_locations(location_union);
147 return shared_from_this();
171 std::dynamic_pointer_cast<const write_location_contextt>(other);
182 return result->update_location_context(location_union,
false);
185 return shared_from_this();
231 existing_locations.insert(locations.begin(), locations.end());
233 return existing_locations;
249 if(
this == before.get())
255 auto before_context =
256 std::dynamic_pointer_cast<const write_location_contextt>(before);
275 before_context->get_last_written_locations();
279 class location_ordert
286 return instruction->location_number > other_instruction->location_number;
290 typedef std::set<goto_programt::const_targett, location_ordert>
293 sorted_locationst lhs_location;
294 for(
const auto &entry : first_write_locations)
296 lhs_location.insert(entry);
299 sorted_locationst rhs_location;
300 for(
const auto &entry : second_write_locations)
302 rhs_location.insert(entry);
306 std::set_intersection(
307 lhs_location.cbegin(),
309 rhs_location.cbegin(),
313 bool all_matched =
intersection.size() == first_write_locations.size() &&
332 std::set<unsigned> sorted_locations;
333 for(
auto location : locations)
335 sorted_locations.insert(location->location_number);
338 for(
auto location_number : sorted_locations)
342 out << location_number;
347 out <<
", " << location_number;
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.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
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.
Base class for all expressions.
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...
abstract_objectt::locationst last_written_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...
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.
CLONE abstract_object_pointert child_abstract_object
An abstract version of a program environment.
std::set< goto_programt::const_targett > locationst
void set_last_written_locations(const abstract_objectt::locationst &locations)
Sets the last written locations for this 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...
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
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...
This is the basic interface of the abstract interpreter with default implementations of the core func...
instructionst::const_iterator const_targett
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.
virtual internal_abstract_object_pointert mutable_clone() 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...