SubstringIndexFor does not help when adding a constant less than or equal to the length of the found string

[panacekcz]

The SubstringIndexFor annotation proposed in typetools #1461 does not help when the added offset is not directly the length of the found string, but a constant known (to the index checker) to be less than or equal to that length.

All the following methods are safe and should ideally not produce any warnings:

import org.checkerframework.common.value.qual.MinLen;

public class IndexOfConstant {
  void direct(String s) {
    int i = s.indexOf("01");
    if (i != -1) {
      s.substring(i + 2);
    }
  }

  void indirect(String s) {
    String c = "01";
    int i = s.indexOf(c);
    if (i != -1) {
      s.substring(i + 2);
    }
  }

  void argument(String s, @MinLen(2) String c) {
    int i = s.indexOf(c);
    if (i != -1) {
      s.substring(i + 2);
    }
  }
}

However, the IndexChecker including #1461 produces warnings for all methods:

IndexOfConstant.java:7: error: [argument.type.incompatible] incompatible types in argument.
      s.substring(i + 2);
                    ^
  found   : @LTLengthOf(value={"s", "s"}, offset={""01".length() - 3", "-3"}) int
  required: @LTEqLengthOf("s") int
IndexOfConstant.java:15: error: [argument.type.incompatible] incompatible types in argument.
      s.substring(i + 2);
                    ^
  found   : @LTLengthOf(value={"s", "s"}, offset={"-3", "c.length() - 3"}) int
  required: @LTEqLengthOf("s") int
IndexOfConstant.java:22: error: [argument.type.incompatible] incompatible types in argument.
      s.substring(i + 2);
                    ^
  found   : @LTLengthOf(value={"s", "s"}, offset={"-3", "c.length() - 3"}) int
  required: @LTEqLengthOf("s") int
3 errors

Occurred in plume-lib, UtilMDE.arglistFromJvm, but that case could be resolved by changing the indexOf call from the string overload to the char version.

[panacekcz]

Related: kelloggm#169, #18.

[panacekcz]

In part duplicate of kelloggm#176.