checker/tests/index/EnumValues.java

import org.checkerframework.common.value.qual.*;

public class EnumValues {

  public static enum Direction {
    NORTH,
    SOUTH,
    EAST,
    WEST
  };

  public static void enumValues() {
    Direction @ArrayLen(4) [] arr4 = Direction.values();
    Direction[] arr = Direction.values();
    Direction a = arr[0];
    Direction b = arr[1];
    Direction c = arr[2];
    Direction d = arr[3];
    // :: error: (array.access.unsafe.high.constant)
    Direction e = arr[4];
  }
}