LtLengthOf and GTENegativeOne implies SubstringIndexFor

[panacekcz]

An expression that is both @GTENeativeOne and @LtLengthOf(value, offset) should be @SubstringIndexFor(value, offset). Code:

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

public class ReturnSubstrinIndexInequality {

    private boolean unknown() {
        throw new RuntimeException();
    }

    public @SubstringIndexFor(value="#1", offset="#2.length()-1") int substringIndexInequality(String a, String b) {
        for (int i = 0; i < a.length() - b.length() + 1; i++) {
            if(unknown())
                return i;
        }

        throw new RuntimeException();
    }

    public @LTLengthOf(value="#1", offset="#2.length-1") int ltLengthOfInequality(int[] a, int[] b) {
        for (int i = 0; i < a.length - b.length + 1; i++) {
            if(unknown())
                return i;
        }

        throw new RuntimeException();
    }

    public @SubstringIndexFor(value="#1", offset="#2.length()-1") int substringIndexFromLtLengthOf(
            String a, String b, @NonNegative @LTLengthOf(value="#1", offset="#2.length()-1") int i) {
        return i;
    }
}

Output:

ReturnSubstrinIndexInequality.java:14: error: [return.type.incompatible] incompatible types in return.
                return i;
                       ^
  found   : @SubstringIndexUnknown int
ReturnSubstrinIndexInequality.java:31: error: [return.type.incompatible] incompatible types in return.
        return i;
               ^
  found   : @SubstringIndexUnknown int
  required: @SubstringIndexFor(value="a", offset="b.length() - 1") int
2 errors

[panacekcz]

Replaced by kelloggm#208.