Class IntervalDomain<Value>

The current abstract value of the lattice.

Maps a set of possible concrete values into an abstract value as abstraction function of the abstract domain (should additionally be provided as static function).

Adds another abstract value to the current abstract value by adding the two lower and upper bounds, respectively.

Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).

Maps the current abstract value into a set of possible concrete values as concretization function of the abstract domain. The result should be Top if the number of concrete values would reach the limit or the resulting set would have infinite many elements.

Checks whether the current abstract value equals to another abstract value.

Extends the lower bound of the current abstract value down to -∞.

Extends the upper bound of the current abstract value up to +∞.

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 other abstract values by creating the least upper bound (LUB) in the lattice.

Checks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.

Creates the maximum between the current abstract value and another abstract value by creating the maximum of the two lower and upper bounds, respectively.

Meets the current abstract value with other abstract values by creating the greatest lower bound (GLB) in the lattice.

Creates the minimum between the current abstract value and another abstract value by creating the minimum of the two lower and upper bounds, respectively.

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.

Subtracts another abstract value from the current abstract value by subtracting the two lower and upper bounds from each other, respectively.

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.