checker/tests/index/LTLengthOfPostcondition.java

import java.util.Arrays;
import org.checkerframework.checker.index.qual.EnsuresLTLengthOf;
import org.checkerframework.checker.index.qual.EnsuresLTLengthOfIf;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;

public class LTLengthOfPostcondition {

  Object[] array;

  @NonNegative @LTEqLengthOf("array") int end;

  @EnsuresLTLengthOf(value = "end", targetValue = "array", offset = "#1 - 1")
  public void shiftIndex(@NonNegative int x) {
    int newEnd = end - x;
    if (newEnd < 0) throw new RuntimeException();
    end = newEnd;
  }

  public void useShiftIndex(@NonNegative int x) {
    // :: error: (argument)
    Arrays.fill(array, end, end + x, null);
    shiftIndex(x);
    Arrays.fill(array, end, end + x, null);
  }

  @EnsuresLTLengthOfIf(expression = "end", result = true, targetValue = "array", offset = "#1 - 1")
  public boolean tryShiftIndex(@NonNegative int x) {
    int newEnd = end - x;
    if (newEnd < 0) {
      return false;
    }
    end = newEnd;
    return true;
  }

  public void useTryShiftIndex(@NonNegative int x) {
    if (tryShiftIndex(x)) {
      Arrays.fill(array, end, end + x, null);
    }
  }
}