| 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.
|