#include <abstract_pointer_object.h>
+ Inheritance diagram for abstract_pointer_objectt:
+ Collaboration diagram for abstract_pointer_objectt:
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
Interface for transforms.
A helper function to evaluate writing to a component of an abstract object.
A helper function to read elements from an array.
Evaluate writing to a pointer's value.
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
Construct an abstract object from the expression.
Get the real type of the variable this abstract object is representing.
Find out if the abstract object is top.
Find out if the abstract object is bottom.
Verify the internal structure of an abstract_object is correct.
Converts to a constant expression if possible.
Converts to an invariant expression.
Print the value of the abstract object.
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.
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}.
Update the write location context for an abstract object.
Update the merge location context for an abstract object.
Apply a visitor operation to all sub elements of this abstract_object.
to_predicate implementation - derived classes will override
Additional Inherited Members
Dump all elements in m1 that are different or missing in m2.
Interface method for the meet operation.
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.
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.
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.
Helper function for base meet.
Helper function to decide if base meet implementation should be used.
Detailed Description
Constructor & Destructor Documentation
◆ abstract_pointer_objectt() [1/2]
abstract_pointer_objectt::abstract_pointer_objectt
(
const typet &
type,
)
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
- Parameters
-
type the type the abstract_object is representing
top is the abstract_object starting as top
bottom is the abstract_object starting as bottom
Definition at line 16 of file abstract_pointer_object.cpp.
◆ abstract_pointer_objectt() [2/2]
abstract_pointer_objectt::abstract_pointer_objectt
(
const exprt &
expr,
)
explicit
- Parameters
-
expr the expression to use as the starting pointer for an abstract object
environment the environment in which the pointer is being created
ns the current namespace
Definition at line 25 of file abstract_pointer_object.cpp.
Member Function Documentation
◆ eval_ptr_comparison()
◆ eval_ptr_diff()
◆ expression_transform()
Interface for transforms.
- Parameters
-
expr the expression to evaluate and find the result of it. This will be the symbol referred to be op0()
operands an abstract_object (pointer) that represent the possible values of each operand
environment the abstract environment in which the expression is being evaluated
ns the current variable namespace
- Returns
- Returns the abstract_object representing the result of this expression to the maximum precision available.
To try and resolve different expressions with the maximum level of precision available.
Reimplemented from abstract_objectt.
Definition at line 37 of file abstract_pointer_object.cpp.
◆ get_statistics()
◆ ptr_comparison_expr()
◆ ptr_diff()
◆ read_dereference()
◆ typecast()
◆ typecast_from_void_ptr()
◆ write()
A helper function to evaluate writing to a component of an abstract object.
More precise abstractions may override this to update what they are storing for a specific component.
- Parameters
-
environment the abstract environment
ns the current namespace
stack the remaining stack of expressions on the LHS to evaluate
specifier the expression uses to access a specific component
value the value we are trying to write to the component
merging_write if true, this and all future writes will be merged with the current value
- Returns
- the abstract_objectt representing the result of writing to a specific component.
Reimplemented from abstract_objectt.
Definition at line 59 of file abstract_pointer_object.cpp.
◆ write_dereference()
Evaluate writing to a pointer's value.
More precise abstractions may override this provide more precise results.
- Parameters
-
environment the abstract environment
ns the namespace
stack the remaining stack of expressions on the LHS to evaluate
value the value we are trying to assign to what the pointer is pointing to
merging_write is it a merging write (i.e. we aren't certain we are writing to this particular pointer therefore the value should be merged with whatever is already there or we are certain we are writing to this pointer so therefore the value can be replaced
- Returns
- A modified abstract object representing this pointer after it has been written to.
Implemented in value_set_pointer_abstract_objectt, constant_pointer_abstract_objectt, and two_value_pointer_abstract_objectt.
The documentation for this class was generated from the following files:
