Index Checker give a false positive

[LoiNguyenCS]

I am having a problem with org.checkerframework.checker.index.IndexChecker. Here is my sample program, which checks if a line contains two consecutive question marks at the beginning.

import org.checkerframework.checker.index.qual.IndexFor;
public class SimpleTestCase
{
  private static boolean atTheBeginning(@IndexFor("#2") int index, String line) {
    return (index==0);
  }

  private static boolean hasDoubleQuestionMarkAtTheBeginning (String line) {
    int i = line.indexOf("??");
    if (i!=-1) {
      return (atTheBeginning(i, line));
    }
    return false;
  }

  public static void main(String[] args) {
    String x = "Hello?World, this is our new program";
    if (hasDoubleQuestionMarkAtTheBeginning(x))
      System.out.println("TRUE");
  }
}

and here is the warning that I get

 return (atTheBeginning(i, line));
                             ^
  found   : @LTEqLengthOf("line") int
  required: @LTLengthOf("line") int

As i is declared as the index of ?? in line, I don't see how i could be equal to the length of line. Is it a bug in the Checker Framework or am I missing something?

[kelloggm]

The problem is the @LTEqLengthOf("this") annotation on indexOf in the annotated JDK: https://github.com/typetools/jdk/blob/4be5323a0462539985fd325199e4a347e4628689/src/java.base/share/classes/java/lang/String.java#L2625.

The annotation is technically correct, but imprecise for most cases. The only time that a non-index (that is equal to the length of the string) can be returned is when the empty string (i.e., "") is both the target string and the string being searched. That is, "".indexOf("") returns 0, which is not an index into "". In all cases where either string is non-empty, the result of indexOf is @LTLengthOf("this"), not @LTEqLengthOf("this").

We should consider adding a special case for calls to indexOf in the Upper Bound Checker that uses the Value Checker to determine if either string parameter is definitely non-empty, in which case this refinement can be applied. That would prevent the false positive warnings in this example (but not all examples caused by these annotations).