Index incremented in a loop over an array

[panacekcz]

Index checker cannot check code that increments an index (other than the loop variable) in a loop.

Example:

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

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

Output:

SecondaryIndex.java:9: error: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound
				b[j] = a[i];
				  ^
  found   : @LTEqLengthOf("a") int
  required: @IndexFor("b") or @LTLengthOf("b") -- an integer less than b's length
SecondaryIndex.java:10: error: [compound.assignment.type.incompatible] incompatible result type in compound assignment.
				++j;
				^
  found   : @LTLengthOf(value="a", offset="-2") int
  required: @LTEqLengthOf("a") int
2 errors