#include <value_set_abstract_object.h>
+ Inheritance diagram for value_set_abstract_objectt:
+ Collaboration diagram for value_set_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.
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.
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.
Static Public Member Functions
Dump all elements in m1 that are different or missing in m2.
Interface method for the meet operation.
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
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.
Setter for updating the stored values.
Update the set of stored values to new_values.
Additional Inherited Members
Detailed Description
Constructor & Destructor Documentation
◆ value_set_abstract_objectt() [1/2]
value_set_abstract_objectt::value_set_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 129 of file value_set_abstract_object.cpp.
◆ value_set_abstract_objectt() [2/2]
value_set_abstract_objectt::value_set_abstract_objectt
(
const exprt &
expr,
)
Member Function Documentation
◆ constrain()
◆ get_values()
◆ index_range_implementation()
◆ make_value_set()
◆ meet_with_value()
◆ merge_with_value()
)
const
overrideprotectedvirtual
◆ mutable_clone()
inlineoverrideprotectedvirtual
◆ output()
void value_set_abstract_objectt::output
(
std::ostream &
out,
)
const
override
◆ 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 274 of file value_set_abstract_object.cpp.
◆ set_top_internal()
void value_set_abstract_objectt::set_top_internal
(
)
overrideprivatevirtual
◆ set_values()
◆ to_constant()
exprt value_set_abstract_objectt::to_constant
(
)
const
overridevirtual
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 190 of file value_set_abstract_object.cpp.
◆ to_interval()
◆ to_predicate_internal()
exprt value_set_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 333 of file value_set_abstract_object.cpp.
◆ value_range_implementation()
Member Data Documentation
◆ max_value_set_size
const size_t value_set_abstract_objectt::max_value_set_size = 10
static
The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top.
Definition at line 54 of file value_set_abstract_object.h.
◆ values
The documentation for this class was generated from the following files:
