#include <value_set_pointer_abstract_object.h>
+ Inheritance diagram for value_set_pointer_abstract_objectt:
+ Collaboration diagram for value_set_pointer_abstract_objectt:
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
Converts to a constant expression if possible.
Getter for the set of stored abstract objects.
Setter for updating the stored values.
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.
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 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.
The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top.
Protected Member Functions
to_predicate implementation - derived classes will override
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.
Update the set of stored values to new_values.
Additional Inherited Members
Dump all elements in m1 that are different or missing in m2.
Interface method for the meet operation.
Detailed Description
Constructor & Destructor Documentation
◆ value_set_pointer_abstract_objectt() [1/3]
value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt
(
const typet &
new_type,
)
◆ value_set_pointer_abstract_objectt() [2/3]
value_set_pointer_abstract_objectt::value_set_pointer_abstract_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 42 of file value_set_pointer_abstract_object.cpp.
◆ value_set_pointer_abstract_objectt() [3/3]
value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt
(
const exprt &
expr,
)
Member Function Documentation
◆ get_values()
◆ merge()
)
const
overrideprotectedvirtual
◆ mutable_clone()
inlineoverrideprotectedvirtual
◆ output()
void value_set_pointer_abstract_objectt::output
(
std::ostream &
out,
)
const
override
◆ ptr_comparison_expr()
exprt value_set_pointer_abstract_objectt::ptr_comparison_expr
(
const exprt &
expr,
)
const
overridevirtual
◆ ptr_diff()
◆ read_dereference()
A helper function to read elements from an array.
More precise abstractions may override this to provide more precise results.
- Parameters
-
env the environment
ns the namespace
- Returns
- An abstract object representing the value being pointed to
Implements abstract_pointer_objectt.
Definition at line 62 of file value_set_pointer_abstract_object.cpp.
◆ resolve_values()
Update the set of stored values to new_values.
Build a new abstract object of the right type if necessary.
- Parameters
-
new_values potentially new set of values
- Returns
- the abstract object representing
new_values (either 'this' or something new)
Definition at line 189 of file value_set_pointer_abstract_object.cpp.
◆ set_values()
◆ to_constant()
exprt value_set_pointer_abstract_objectt::to_constant
(
)
const
inlineoverridevirtual
Converts to a constant expression if possible.
- Returns
- Returns an exprt representing the value if the value is known and constant. Otherwise returns the nil expression
If abstract element represents a single value, then that value, otherwise nil. E.G. if it is an interval then this will be x if it is [x,x] This is the (sort of) dual to the constant_exprt constructor that allows an object to be built from a value.
Reimplemented from abstract_objectt.
Definition at line 37 of file value_set_pointer_abstract_object.h.
◆ to_predicate_internal()
exprt value_set_pointer_abstract_objectt::to_predicate_internal
(
const exprt &
name )
const
overrideprotectedvirtual
to_predicate implementation - derived classes will override
- Parameters
-
name - the variable name to substitute into the expression
- Returns
- Returns an exprt representing the object as an invariant.
Reimplemented from abstract_objectt.
Definition at line 228 of file value_set_pointer_abstract_object.cpp.
◆ typecast()
◆ 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.
Implements abstract_pointer_objectt.
Definition at line 83 of file value_set_pointer_abstract_object.cpp.
Member Data Documentation
◆ max_value_set_size
const size_t value_set_pointer_abstract_objectt::max_value_set_size = 10
static
◆ values
The documentation for this class was generated from the following files:
