panacekcz / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
0 stars 0 forks source link

SubstringIndexFor does not help when adding a length of a prefix of the found string #23

Open panacekcz opened 6 years ago

panacekcz commented 6 years ago

The SubstringIndexFor annotation proposed in typetools #1461 does not help when the added offset is a length of a prefix of the found string.

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

public class IndexOfPrefix {
  void direct(String s, String t, String u) {
    int i = s.indexOf(t + u);
    if (i != -1) {
      s.substring(i + t.length());
    }
  }

  void indirect(String s, String t, String u) {
    String tu = t + u;
    int i = s.indexOf(tu);
    if (i != -1) {
      s.substring(i + t.length());
    }
  }
}

However, the Index Checker including #1461 produces warnings for both methods:

IndexOfPrefix.java:5: error: [argument.type.incompatible] incompatible types in argument.
      s.substring(i + t.length());
                    ^
  found   : @LTLengthOf(value={"s", "s", "t"}, offset={"-t.length() - 1", "?.length() - t.length() - 1", "-i - 1"}) int
  required: @LTEqLengthOf("s") int
IndexOfPrefix.java:13: error: [argument.type.incompatible] incompatible types in argument.
      s.substring(i + t.length());
                    ^
  found   : @LTLengthOf(value={"s", "s", "t"}, offset={"-t.length() - 1", "tu.length() - t.length() - 1", "-i - 1"}) int
  required: @LTEqLengthOf("s") int
2 errors

Occurred in plume-lib, OptionsDoclet.refill(String,int,int,int).

panacekcz commented 6 years ago

A solution could potentially be built on sequence length inequality annotations (#11).