checker/tests/index/OffsetExample.java

import java.util.List;
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.common.value.qual.MinLen;

@SuppressWarnings("lowerbound")
public class OffsetExample {
  void example1(int @MinLen(2) [] a) {
    int j = 2;
    int x = a.length;
    int y = x - j;
    for (int i = 0; i < y; i++) {
      a[i + j] = 1;
    }
  }

  void example2(int @MinLen(2) [] a) {
    int j = 2;
    int x = a.length;
    int y = x - j;
    a[y] = 0;
    for (int i = 0; i < y; i++) {
      a[i + j] = 1;
      a[j + i] = 1;
      a[i + 0] = 1;
      a[i - 1] = 1;
      // ::error: (array.access.unsafe.high)
      a[i + 2 + j] = 1;
    }
  }

  void example3(int @MinLen(2) [] a) {
    int j = 2;
    for (int i = 0; i < a.length - 2; i++) {
      a[i + j] = 1;
    }
  }

  void example4(int[] a, int offset) {
    int max_index = a.length - offset;
    for (int i = 0; i < max_index; i++) {
      a[i + offset] = 0;
    }
  }

  void example5(int[] a, int offset) {
    for (int i = 0; i < a.length - offset; i++) {
      a[i + offset] = 0;
    }
  }

  void test(@IndexFor("#3") int start, @IndexOrHigh("#3") int end, int[] a) {
    if (end > start) {
      // If start == 0, then end - start is end.  end might be equal to the length of a.  So
      // the array access might be too high.
      // ::error: (array.access.unsafe.high)
      a[end - start] = 0;
    }

    if (end > start) {
      a[end - start - 1] = 0;
    }
  }

  public static boolean isSubarray(Object[] a, Object[] sub, int a_offset) {
    int a_len = a.length - a_offset;
    int sub_len = sub.length;
    if (a_len < sub_len) {
      return false;
    }
    for (int i = 0; i < sub_len; i++) {
      if (sub[i] == a[a_offset + i]) {
        return false;
      }
    }
    return true;
  }

  public void test2(int[] a, List<Object> b) {
    int b_size = b.size();
    Object[] result = new Object[a.length + b_size];
    for (int i = 0; i < b_size; i++) {
      result[i + a.length] = b.get(i);
    }
  }
}