|
Class Summary |
| 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 scalars 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 used to evaluate single double scalars. |
| SingleScalar |
Abstract base class used to evaluate single long scalars. |
| 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. |