CompleteOneOfScalar |
Tracks every unique value and how many times it occurs.
|
CompleteOneOfScalar.Info |
Information about each value encountered.
|
IsPointer |
IsPointer is an invariant that heuristically determines whether an integer represents a pointer
(a 32-bit memory address).
|
LowerBound |
Represents the invariant x >= c , where c is a constant and
x is a long scalar.
|
LowerBoundFloat |
Represents the invariant x >= c , where c is a constant and
x is a double scalar.
|
Modulus |
Represents the invariant x == r (mod m) where x is a long scalar variable,
r is the (constant) remainder, and m is the (constant) modulus.
|
NonModulus |
Represents long scalars that are never equal to r (mod m) where all other numbers in the
same range (i.e., all the values that x doesn't take from min(x) to
max(x) ) are equal to r (mod m) .
|
NonZero |
Represents long scalars that are non-zero.
|
NonZeroFloat |
Represents double scalars that are non-zero.
|
OneOfFloat |
Represents double variables that take on only a few distinct values.
|
OneOfScalar |
Represents long variables that take on only a few distinct values.
|
Positive |
Represents the invariant x > 0 where x is a long scalar.
|
RangeFloat |
Baseclass for unary range based invariants.
|
RangeFloat.EqualMinusOne |
Internal invariant representing double scalars that are equal to minus one.
|
RangeFloat.EqualOne |
Internal invariant representing double scalars that are equal to one.
|
RangeFloat.EqualZero |
Internal invariant representing double scalars that are equal to zero.
|
RangeFloat.GreaterEqual64 |
Internal invariant representing double scalars that are greater than or equal to 64.
|
RangeFloat.GreaterEqualZero |
Internal invariant representing double scalars that are greater than or equal to 0.
|
RangeInt |
Baseclass for unary range based invariants.
|
RangeInt.BooleanVal |
Internal invariant representing longs whose values are always 0 or 1.
|
RangeInt.Bound0_63 |
Internal invariant representing longs whose values are between 0 and 63.
|
RangeInt.EqualMinusOne |
Internal invariant representing long scalars that are equal to minus one.
|
RangeInt.EqualOne |
Internal invariant representing long scalars that are equal to one.
|
RangeInt.EqualZero |
Internal invariant representing long scalars that are equal to zero.
|
RangeInt.Even |
Invariant representing longs whose values are always even.
|
RangeInt.GreaterEqual64 |
Internal invariant representing long scalars that are greater than or equal to 64.
|
RangeInt.GreaterEqualZero |
Internal invariant representing long scalars that are greater than or equal to 0.
|
RangeInt.PowerOfTwo |
Invariant representing longs whose values are always a power of 2 (exactly one bit is set).
|
SingleFloat |
Abstract base class for invariants over one variable of type double .
|
SingleScalar |
Abstract base class for invariants over one numeric (scalar) variable, such as x != 0 .
|
UpperBound |
Represents the invariant x <= c , where c is a constant and
x is a long scalar.
|
UpperBoundFloat |
Represents the invariant x <= c , where c is a constant and
x is a double scalar.
|