checker/tests/index/OnlyCheckSubsequenceWhenAssigningToArray.java

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

public class OnlyCheckSubsequenceWhenAssigningToArray {
  @HasSubsequence(subsequence = "this", from = "this.start", to = "this.end")
  int[] array;

  final @IndexFor("array") int start;

  final @IndexOrHigh("array") int end;

  private OnlyCheckSubsequenceWhenAssigningToArray(
      @IndexFor("array") int s, @IndexOrHigh("array") int e) {
    start = s;
    end = e;
  }

  void testAssignmentToArrayElement(@IndexFor("this") int x, int y) {
    array[start + x] = y;
  }

  void testAssignmentToArray(int[] a) {
    // :: error: to.not.ltel :: error: from.gt.to
    array = a;
  }
}