|
| | abstract_aggregate_objectt (const typet &type, bool tp, bool bttm) |
| |
| | abstract_aggregate_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.
|
| |
| 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.
|
| |
| void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
| |
| | 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.
|
| |
| | abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
| | Construct an abstract object from the expression.
|
| |
| virtual | ~abstract_objectt () |
| |
| virtual const typet & | type () const |
| | Get the real type of the variable this abstract object is representing.
|
| |
| virtual bool | is_top () const |
| | Find out if the abstract object is top.
|
| |
| virtual bool | is_bottom () const |
| | Find out if the abstract object is bottom.
|
| |
| virtual bool | verify () const |
| | Verify the internal structure of an abstract_object is correct.
|
| |
| virtual exprt | to_constant () const |
| | Converts to a constant expression if possible.
|
| |
| exprt | to_predicate (const exprt &name) const |
| | Converts to an invariant expression.
|
| |
| virtual void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const |
| | Print the value of the abstract object.
|
| |
| 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 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}.
|
| |
| virtual abstract_object_pointert | write_location_context (const locationt &location) const |
| | Update the write location context for an abstract object.
|
| |
| virtual abstract_object_pointert | merge_location_context (const locationt &location) const |
| | Update the merge location context for an abstract object.
|
| |
| 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.
|
| |
| 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
|
| |
Inheritance diagram for abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >:
1.9.8