Class UpperBoundAnnotatedTypeFactory

All Implemented Interfaces:

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.