checker/tests/index/Issue3207.java

// Test case for https://tinyurl.com/cfissue/3207

import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.common.value.qual.MinLen;

public class Issue3207 {

  void m(int @MinLen(1) [] arr) {
    @LTLengthOf("arr") int j = 0;
  }

  void m2(int @MinLen(1) [] @MinLen(1) [] arr) {
    @LTLengthOf("arr[0]") int j = 0;
  }

  void m3(int @MinLen(1) [] @MinLen(1) [] arr) {
    int @MinLen(1) [] arr0 = arr[0];
    @LTLengthOf("arr0") int j = 0;
  }
}