AbstractType of an abstract element of the abstract domain representing possible elements (excludes Top and Bot)
Type of the Top element of the abstract domain representing all possible elements
Type of the Bottom element of the abstract domain representing no possible elements
Type of the current abstract value in the abstract domain (defaults to Value or Top or Bot)
Type of an abstract element of the abstract domain representing possible elements (excludes Top and Bot)
Type of the Top element of the abstract domain representing all possible elements
Type of the Bottom element of the abstract domain representing no possible elements
Type of the current abstract value in the abstract domain (defaults to Value or Top or Bot)
StaticjoinJoins an array of abstract values by joining the first abstract value with the other values in the array. The provided array of abstract values must not be empty or a default value must be provided!
StaticmeetMeets an array of abstract values by meeting the first abstract value with the other values in the array. The provided array of abstract values must not be empty or a default value must be provided!
StatictoConverts an element of an abstract domain into a string.
AbstractbottomGets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
AbstractcreateChecks whether the current abstract value equals to another abstract value.
Protected AbstractequalsAbstractisChecks whether the current abstract value is the Bottom element of the complete lattice.
AbstractisChecks whether the current abstract value is the Top element of the complete lattice.
AbstractisChecks whether the current abstract value is an actual value of the complete lattice (this may include the Top or Bottom element if they are also values and no separate symbols, for example).
Joins the current abstract value with multiple other abstract values.
Protected AbstractjoinProtected AbstractjsonifyChecks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.
Protected AbstractleqMeets the current abstract value with multiple other abstract values.
Protected AbstractmeetNarrows the current abstract value with another abstract value as a sound over-approximation of the meet (greatest lower bound) to refine the value after widening.
Protected OptionalnarrowProtected AbstractstringifyConverts the lattice into a JSON serializable value.
AbstracttopGets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).
Converts the lattice into a human-readable string.
Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration.
Protected Optionalwiden
An abstract domain as complete lattice with a widening and narrowing operator. All operations of value abstract domains should not modify the domain in-place but return new values using create.