|
| | abstract_pointer_objectt (const typet &type, bool top, bool bottom) |
| | Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...
|
| |
| | abstract_pointer_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
| |
| abstract_object_pointert | expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override |
| | Interface for transforms. More...
|
| |
| 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. More...
|
| |
| void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
| |
| virtual abstract_object_pointert | read_dereference (const abstract_environmentt &env, const namespacet &ns) const =0 |
| | A helper function to read elements from an array. More...
|
| |
| virtual abstract_object_pointert | write_dereference (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const =0 |
| | Evaluate writing to a pointer's value. More...
|
| |
| virtual abstract_object_pointert | typecast (const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const =0 |
| |
| virtual abstract_object_pointert | ptr_diff (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0 |
| |
| virtual exprt | ptr_comparison_expr (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0 |
| |
| | abstract_objectt (const typet &type, bool top, bool bottom) |
| | Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...
|
| |
| | abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
| | Construct an abstract object from the expression. More...
|
| |
| virtual | ~abstract_objectt () |
| |
| virtual const typet & | type () const |
| | Get the real type of the variable this abstract object is representing. More...
|
| |
| virtual bool | is_top () const |
| | Find out if the abstract object is top. More...
|
| |
| virtual bool | is_bottom () const |
| | Find out if the abstract object is bottom. More...
|
| |
| virtual bool | verify () const |
| | Verify the internal structure of an abstract_object is correct. More...
|
| |
| virtual exprt | to_constant () const |
| | Converts to a constant expression if possible. More...
|
| |
| exprt | to_predicate (const exprt &name) const |
| | Converts to an invariant expression. More...
|
| |
| virtual void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const |
| | Print the value of the abstract object. More...
|
| |
| 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. More...
|
| |
| virtual abstract_object_pointert | meet (const abstract_object_pointert &other) const |
| | Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}. More...
|
| |
| virtual abstract_object_pointert | write_location_context (const locationt &location) const |
| | Update the write location context for an abstract object. More...
|
| |
| virtual abstract_object_pointert | merge_location_context (const locationt &location) const |
| | Update the merge location context for an abstract object. More...
|
| |
| abstract_object_pointert | make_top () const |
| |
| abstract_object_pointert | clear_top () const |
| |
| virtual abstract_object_pointert | unwrap_context () const |
| |
| 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. More...
|
| |
| virtual size_t | internal_hash () const |
| |
| virtual bool | internal_equality (const abstract_object_pointert &other) const |
| |
| virtual exprt | to_predicate_internal (const exprt &name) const |
| | to_predicate implementation - derived classes will override More...
|
| |
|
| typedef goto_programt::const_targett | locationt |
| |
| typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | shared_mapt |
| |
| static void | dump_map (std::ostream out, const shared_mapt &m) |
| |
| 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. More...
|
| |
| static combine_result | merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode) |
| |
| static combine_result | merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode) |
| |
| static combine_result | meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2) |
| | Interface method for the meet operation. More...
|
| |
| template<class T > |
| using | internal_sharing_ptrt = std::shared_ptr< T > |
| |
| typedef internal_sharing_ptrt< class abstract_objectt > | internal_abstract_object_pointert |
| |
| virtual internal_abstract_object_pointert | mutable_clone () 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, then would return itself. More...
|
| |
| 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() since we want the specific. More...
|
| |
| virtual abstract_object_pointert | merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const |
| | Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More...
|
| |
| abstract_object_pointert | abstract_object_meet (const abstract_object_pointert &other) const |
| | Helper function for base meet. More...
|
| |
| bool | should_use_base_meet (const abstract_object_pointert &other) const |
| | Helper function to decide if base meet implementation should be used. More...
|
| |
| void | set_top () |
| |
| void | set_not_top () |
| |
| void | set_not_bottom () |
| |
Definition at line 20 of file abstract_pointer_object.h.
Inheritance diagram for abstract_pointer_objectt: