IntervalDomain class

Interval domain for tracking integer value ranges.

Represents values as min, max where min, max ∈ ℤ ∪ {-∞, +∞}. Used for array bounds checking and integer overflow detection.

Implemented types

Constructors

IntervalDomain(int? min, int? max): const
IntervalDomain.arrayIndex(int length): Creates an interval 0, n-1 for array indices.
factory
IntervalDomain.constant(int value): Creates an interval from a single constant.
factory

bottom → IntervalDomain: Returns the bottom element (⊥).
no setteroverride
hashCode → int: The hash code for this object.
no setteroverride
isBottom → bool: Checks if this is the bottom element.
no setteroverride
isTop → bool: Checks if this is the top element.
no setteroverride
max → int?: final
min → int?: final
runtimeType → Type: A representation of the runtime type of the object.
no setterinherited
top → IntervalDomain: Returns the top element (⊤).
no setteroverride

add(IntervalDomain other) → IntervalDomain
containsValue(int value) → bool: Checks if this interval contains a specific value.
divide(IntervalDomain other) → IntervalDomain: Integer division of two intervals.
isLessThan(IntervalDomain other) → bool: Checks if this interval satisfies a < b relation.
isSubsetOf(IntervalDomain other) → bool: Checks if this value is less than or equal to another (⊑).
override
isValidArrayIndex(int length) → bool: Checks if value is definitely within bounds [0, length).
join(IntervalDomain other) → IntervalDomain: Join operation (⊔): least upper bound of two abstract values.
override
meet(IntervalDomain other) → IntervalDomain: Meet operation (⊓): greatest lower bound of two abstract values.
override
modulo(IntervalDomain other) → IntervalDomain: Modulo operation on two intervals.
multiply(IntervalDomain other) → IntervalDomain
narrow(IntervalDomain other) → IntervalDomain: Narrowing operation (△): refines over-approximation after widening.
override
noSuchMethod(Invocation invocation) → dynamic: Invoked when a nonexistent method or property is accessed.
inherited
subtract(IntervalDomain other) → IntervalDomain
toString() → String: A string representation of this object.
override
widen(IntervalDomain other) → IntervalDomain: Widening operation (∇): ensures termination in fixpoint iteration.
override