40 const std::stack<exprt> &stack,
41 const exprt &specifier,
43 bool merging_write)
const
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();
53 std::dynamic_pointer_cast<liveness_contextt>(updated->mutable_clone());
55 std::dynamic_pointer_cast<const liveness_contextt>(value);
57 result->set_location(value_context->get_location());
76 auto cast_other = std::dynamic_pointer_cast<const liveness_contextt>(other);
80 auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
91 auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
99 if(merged == shared_from_this())
100 return shared_from_this();
103 std::dynamic_pointer_cast<liveness_contextt>(merged->mutable_clone());
104 updated->assign_location.reset();
112 auto result = std::dynamic_pointer_cast<liveness_contextt>(
mutable_clone());
113 result->set_last_written_locations(locations);
114 result->set_location(*locations.cbegin());
139 out <<
" @ [" <<
get_location()->location_number <<
"]";
141 out <<
" @ [undefined]";
148 return shared_from_this();
150 auto update = std::dynamic_pointer_cast<liveness_contextt>(
mutable_clone());
151 update->assign_location = location;
153 update->set_child(updated_child);
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...
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.
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...
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...