16 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
17 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
72 const bool update_sub_elements)
const override;
87 return element->update_location_context(
locations,
true);
110 const std::stack<exprt> &stack,
111 const exprt &specifier,
113 bool merging_write)
const override;
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...
const typet & type() const override
Get the real type of the variable this abstract object is representing.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
const locationst & locations
location_update_visitort(const locationst &locations)
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.
virtual ~write_location_contextt()
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...