checker/tests/index/PlumeFailMin.java

// Test case for eisop Issue 22:
// https://github.com/eisop/checker-framework/issues/22

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

abstract class PlumeFailMin {
  void ok() {
    String @MinLen(1) [] args = getArrayOk();
    @IndexOrHigh("args") int x = 1;
  }

  abstract String @MinLen(1) [] getArrayOk();

  void fail() {
    // Workaround by casting.
    @SuppressWarnings({"index", "value"})
    String @MinLen(1) [] args = (String @MinLen(1) []) getArrayFail();
    @IndexOrHigh("args") int x = 1;
  }

  abstract String[] getArrayFail();
}