Inference of IndexOrHigh after a for loop

[panacekcz]

The index checker does not infer the @IndexOrHigh qualifier for a variable that has been used as an index to iterate over an array in a for loop. After the loop, the variable contains the length of an array (if the loop is exitted normally) or an index for the array (if the loop is exitted by break). Therefore, it can be safely considered to be @IndexOrHigh for the array.

Encountered in Guava.

Could it be a limitation of the dataflow implementation?

Code:

import org.checkerframework.checker.index.qual.IndexOrHigh;

public class IndexOrHighInfer {
	void m(Object[] a) {
	    int i;
	    for (i = 0; i < a.length; i++) {
	      if(a[i] == null)
	    	  break;
	    }
	    
	    @IndexOrHigh("a") int j = i;
	}
}

Output:

IndexOrHighInfer.java:11: error: [assignment.type.incompatible] incompatible types in assignment.
	    @IndexOrHigh("a") int j = i;
	                              ^
  found   : @UpperBoundUnknown int
  required: @LTEqLengthOf("a") int
1 error

Expected: no warning.