26 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
27 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
48 internal_abstract_object_pointert mutable_clone() const override \
50 typedef std::remove_const< \
51 std::remove_reference<decltype(*this)>::type>::type current_typet; \
52 return internal_abstract_object_pointert(new current_typet(*this)); \
130 virtual bool is_top()
const;
140 virtual bool verify()
const;
165 const std::vector<abstract_object_pointert> &operands,
199 const std::stack<exprt> &stack,
200 const exprt &specifier,
202 bool merging_write)
const;
243 return this != before.get();
260 bool &out_modifications);
274 bool &out_modifications);
297 const bool update_sub_elements)
const;
303 return shared_from_this();
313 return shared_from_this();
316 clone->set_not_top();
346 return shared_from_this();
351 return std::hash<abstract_object_pointert>{}(shared_from_this());
356 return shared_from_this() == other;
467 return s->internal_hash();
478 return left->internal_equality(right);
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
virtual bool internal_equality(const abstract_object_pointert &other) const
virtual exprt to_constant() const
Converts to a constant expression if possible.
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
abstract_objectt(const typet &type)
virtual bool has_been_modified(const abstract_object_pointert before) const
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
virtual bool is_top() const
Find out if the abstract object is top.
static void dump_map(std::ostream out, const shared_mapt &m)
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual 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
A helper function to evaluate writing to a component of an abstract object.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
virtual abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
virtual void set_not_top_internal()
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
virtual void set_top_internal()
virtual abstract_object_pointert abstract_object_meet_internal(const abstract_object_pointert &other) const
Helper function for base meet, in case additional work was needed.
static void dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
Dump all elements in m1 that are different or missing in m2.
std::shared_ptr< T > internal_sharing_ptrt
abstract_object_pointert make_top() const
virtual size_t internal_hash() const
abstract_object_pointert abstract_object_merge(const abstract_object_pointert other) const
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
virtual abstract_object_pointert update_location_context(const locationst &locations, const bool update_sub_elements) const
Update the location context for an abstract object, potentially propogating the update to any childre...
virtual abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const
Apply a visitor operation to all sub elements of this abstract_object.
bool should_use_base_merge(const abstract_object_pointert other) const
To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom()...
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
abstract_object_pointert clear_top() const
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_mapt
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.
virtual abstract_object_pointert unwrap_context() const
std::set< goto_programt::const_targett > locationst
typet t
To enforce copy-on-write these are private and have read-only accessors.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual ~abstract_objectt()
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
A constant literal expression.
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.
abstract_object_pointert argument_typet
bool operator()(argument_typet const &left, argument_typet const &right) const noexcept
abstract_object_pointert argument_typet
result_typet operator()(argument_typet const &s) const noexcept
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0