0 is a valid SubstringIndexFor if the argument is not longer than receiver

[panacekcz]

If the argument is empty, 0 is a valid @SubstringIndexFor. More generally, if the argument is not longer than receiver. This case would need #11.

Code, containing generalized examples:

import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.SubstringIndexFor;

public class ReturnSubstringIndexZero {
    public @SubstringIndexFor(value="#1", offset="#2.length()-1") int substringIndexOfEmpty(String a, String b) {
        if(b.length() == 0)
            return 0;
        else
            throw new RuntimeException();
    }

    public @SubstringIndexFor(value="#1", offset="#2.length()-1") int substringIndexOfShorter(String a, String b) {
        if(b.length() <= a.length())
            return 0;
        else
            throw new RuntimeException();
    }

    public @SubstringIndexFor(value="#1", offset="#2.length()-1") int substringIndexOfShorterConst(String a, String b) {
        if(b.length() + 4 <= a.length())
            return 4;
        else
            throw new RuntimeException();
    }

    public @LTLengthOf(value="#1", offset="#2.length-1") int ltLengthOfEmpty(int[] a, int[] b) {
        if(b.length == 0)
            return 0;
        else
            throw new RuntimeException();
    }

    public @LTLengthOf(value="#1", offset="#2.length-1") int ltLengthOfShorter(int[] a, int[] b) {
        if(b.length <= a.length)
            return 0;
        else
            throw new RuntimeException();
    }
}

Output:

ReturnSubstringIndexZero.java:7: error: [return.type.incompatible] incompatible types in return.
            return 0;
                   ^
  found   : @SubstringIndexUnknown int
  required: @SubstringIndexFor(value="a", offset="b.length() - 1") int
ReturnSubstringIndexZero.java:14: error: [return.type.incompatible] incompatible types in return.
            return 0;
                   ^
  found   : @SubstringIndexUnknown int
  required: @SubstringIndexFor(value="a", offset="b.length() - 1") int
ReturnSubstringIndexZero.java:21: error: [return.type.incompatible] incompatible types in return.
            return 4;
                   ^
  found   : @SubstringIndexUnknown int
  required: @SubstringIndexFor(value="a", offset="b.length() - 1") int
ReturnSubstringIndexZero.java:28: error: [return.type.incompatible] incompatible types in return.
            return 0;
                   ^
  found   : @UpperBoundUnknown int
  required: @LTLengthOf(value="a", offset="b.length - 1") int
ReturnSubstringIndexZero.java:35: error: [return.type.incompatible] incompatible types in return.
            return 0;
                   ^
  found   : @UpperBoundUnknown int
  required: @LTLengthOf(value="a", offset="b.length - 1") int
5 errors

[panacekcz]

Replaced by kelloggm#207.