#include <abstract_value_object.h>
+ Inheritance diagram for abstract_value_objectt:
+ Collaboration diagram for abstract_value_objectt:
Interface for transforms.
A helper function to evaluate writing to a component of an abstract object.
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.
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
Protected Member Functions
Attempts to do a value/value merge if both are constants, otherwise falls back to the parent merge.
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}.
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.
Helper function for base meet.
Helper function to decide if base meet implementation should be used.
Additional Inherited Members
Dump all elements in m1 that are different or missing in m2.
Interface method for the meet operation.
Detailed Description
Member Typedef Documentation
◆ abstract_value_pointert
Constructor & Destructor Documentation
◆ abstract_value_objectt() [1/2]
abstract_value_objectt::abstract_value_objectt
(
const typet &
type,
)
inline
◆ abstract_value_objectt() [2/2]
abstract_value_objectt::abstract_value_objectt
(
const exprt &
expr,
)
inline
Member Function Documentation
◆ as_value()
◆ constrain()
◆ 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.
Reimplemented from abstract_objectt.
Definition at line 172 of file abstract_value_object.cpp.
◆ index_range()
◆ index_range_implementation()
◆ meet()
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}.
- Parameters
-
other pointer to the abstract object to meet
- Returns
- the resulting abstract object pointer
Reimplemented from abstract_objectt.
Definition at line 205 of file abstract_value_object.cpp.
◆ meet_with_value()
◆ merge()
)
const
finalprotectedvirtual
Attempts to do a value/value merge if both are constants, otherwise falls back to the parent merge.
- Parameters
-
other the abstract object to merge with
widen_mode Indicates if this is a widening merge
- Returns
- Returns the result of the merge
Reimplemented from abstract_objectt.
Definition at line 192 of file abstract_value_object.cpp.
◆ merge_with_value()
)
const
protectedpure virtual
◆ to_interval()
◆ value_range()
◆ value_range_implementation()
◆ 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 181 of file abstract_value_object.cpp.
The documentation for this class was generated from the following files:
