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

[panacekcz]

If the argument (the substring searched for) is empty, then 0 is a valid @SubstringIndexFor.
More generally, 0 is valid if the argument is not longer than the receiver. This would require knowing about sequence length inequalities (#202).

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

This issue has been originally tracked as panacekcz#25.