Class UpperBoundAnnotatedTypeFactory

  • All Implemented Interfaces:
    AnnotationProvider

    public class UpperBoundAnnotatedTypeFactory
    extends BaseAnnotatedTypeFactoryForIndexChecker
    Implements the introduction rules for the Upper Bound Checker.

    Rules implemented by this class:

    • 1. Math.min has unusual semantics that combines annotations for the UBC.
    • 2. The return type of Random.nextInt depends on the argument, but is not equal to it, so a polymorphic qualifier is insufficient.
    • 3. Unary negation on a NegativeIndexFor (from the SearchIndex Checker) results in a LTLengthOf for the same arrays.
    • 4. Right shifting by a constant between 0 and 30 preserves the type of the left side expression.
    • 5. If either argument to a bitwise and expression is non-negative, the and expression retains that argument's upperbound type. If both are non-negative, the result of the expression is the GLB of the two.
    • 6. if numerator ≥ 0, then numerator % divisor ≤ numerator
    • 7. if divisor ≥ 0, then numerator % divisor < divisor
    • 8. If the numerator is an array length access of an array with non-zero length, and the divisor is greater than one, glb the result with an LTL of the array.
    • 9. if numeratorTree is a + b and divisor greater than 1, and a and b are less than the length of some sequence, then (a + b) / divisor is less than the length of that sequence.
    • 10. Special handling for Math.random: Math.random() * array.length is LTL array.