Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
The current abstract value of the lattice.
StaticbottomStaticfromStaticjoinJoins 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!
StatictopStatictoConverts an element of an abstract domain into a string.
Adds an numeric abstract value to this numeric abstract value.
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
Creates an abstract value of the lattice for a given value.
Divides this numeric abstract value by another numeric abstract value.
Checks whether the current abstract value equals to another abstract value.
ProtectedequalsAbstracts a list of concrete values into an abstract value of the value abstract domain.
Checks whether the current abstract value is the Bottom element of the complete lattice.
Checks whether the current abstract value is the Top element of the complete lattice.
Checks 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 another abstract value by creating the least upper bound (LUB) in the lattice.
Joins the current abstract value with multiple other abstract values.
ProtectedjoinProtectedjsonifyChecks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.
ProtectedleqGets the maximum of this numeric abstract value and another numeric abstract value.
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Meets the current abstract value with multiple other abstract values.
ProtectedmeetGets the minimum of this numeric abstract value and another numeric abstract value.
Multiplies this numeric abstract value with another numeric abstract value.
Narrows 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.
ProtectednarrowNegates this numeric abstract value.
Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value).
Ternary for the returned satisfiability result
ProtectedstringifySubtracts an numeric abstract value from this numeric abstract value.
Converts the lattice into a JSON serializable value.
Gets 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.
Extends the lower bound of the current abstract value down to 0.
Extends the upper bound of the current abstract value up to +∞.
Protectedwiden
The positive interval abstract domain as positive intervals with possibly zero lower bounds and infinite upper bounds representing possible numeric values. The Bottom element is defined as Bottom symbol and the Top element is defined as the interval [0, +∞].