SameLen annotations on the elements of arrays/sequences do not work correctly

[kelloggm]

They also behave differently for Strings and other arrays. In particular, a String array whose elements are annotated as SameLen of some other array is permitted to be assigned into another variable with the same annotation (test2 below), but an array annotated similarly is not (test4). test1 and test3 show expected use cases; only the version with a String array issues warnings.

Consider the following code:

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.SameLen;

public class SameLenOnArrayElements {
    @SameLen("this.oneDarray") String[] stringArray;
    @SameLen("this.oneDarray") int[][] twoDarray;
    int[] oneDarray;

    void test1(@IndexFor("this.stringArray") int i) {
        String s = stringArray[i];
        int index = s.indexOf('c');
        if (index != -1) {
            oneDarray[index] = 6;
        }
    }

    void test2(@IndexFor("this.stringArray") int i) {
        String s = stringArray[i];
        @SameLen({"s", "oneDarray"}) String t = s;
    }

    void test3(@IndexFor("this.twoDarray") int i) {
        int[] arr = twoDarray[i];
        for (int j = 0; j < arr.length; ++j) {
            oneDarray[j] = 7;
        }
    }

    void test4(@IndexFor("this.twoDarray") int i) {
        int[] arr = twoDarray[i];
        int @SameLen({"arr", "oneDarray"}) [] arr2 = arr;
    }
}

Output:

tests/index/SameLenOnArrayElements.java:29: error: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound
            oneDarray[j] = 7;
                      ^
  found   : @LTLengthOf(value={"arr", "this.twoDarray[i]"}, offset={"0", "0"}) int
  required: @IndexFor("this.oneDarray") or @LTLengthOf("this.oneDarray") -- an integer less than this.oneDarray's length
tests/index/SameLenOnArrayElements.java:35: error: [assignment.type.incompatible] incompatible types in assignment.
        int @SameLen({"arr", "oneDarray"}) [] arr2 = arr;
                                                     ^
  found   : @SameLenUnknown int @SameLen({"arr", "this.twoDarray[i]"}) []
  required: @SameLenUnknown int @SameLen({"arr", "this.oneDarray"}) []
2 errors

Expected: no output

[panacekcz]

The declaration for twoDarray should be int @SameLen("this.oneDarray") [][] twoDarray;. However, the output is the same.