Go to the documentation of this file.
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;
471 return s->internal_hash();
482 return left->internal_equality(right);
486 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
virtual bool internal_equality(const abstract_object_pointert &other) const
result_typet operator()(argument_typet const &s) const noexcept
static void dump_map(std::ostream out, const shared_mapt &m)
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.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
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 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
The type of an expression, extends irept.
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()...
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
virtual size_t internal_hash() const
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
Base class for all expressions.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
abstract_object_pointert clear_top() const
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
abstract_object_pointert argument_typet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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...
bool operator()(argument_typet const &left, argument_typet const &right) const noexcept
virtual ~abstract_objectt()
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_mapt
std::set< goto_programt::const_targett > locationst
virtual exprt to_constant() const
Converts to a constant expression if possible.
abstract_object_pointert make_top() const
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.
virtual void set_not_top_internal()
std::set< abstract_object_pointert > abstract_object_visitedt
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...
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
abstract_object_pointert argument_typet
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
virtual abstract_object_pointert unwrap_context() 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,...
Statistics gathering for the variable senstivity domain.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
std::shared_ptr< T > internal_sharing_ptrt
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 void set_top_internal()
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
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...
virtual bool is_bottom() const
Find out if the abstract object is bottom.
A constant literal expression.
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0
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.
virtual internal_abstract_object_pointert mutable_clone() const
typet t
To enforce copy-on-write these are private and have read-only accessors.
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.
abstract_objectt(const typet &type)