checker/tests/index/MinLenFieldInvar.java

package fieldinvar;

import org.checkerframework.common.value.qual.BottomVal;
import org.checkerframework.common.value.qual.MinLen;
import org.checkerframework.common.value.qual.MinLenFieldInvariant;
import org.checkerframework.framework.qual.FieldInvariant;

public class MinLenFieldInvar {
  class Super {
    public final int @MinLen(2) [] minlen2;

    public Super(int @MinLen(2) [] minlen2) {
      this.minlen2 = minlen2;
    }
  }

  // :: error: (field.invariant.not.subtype)
  @MinLenFieldInvariant(field = "minlen2", minLen = 1)
  class InvalidSub extends Super {
    public InvalidSub() {
      super(new int[] {1, 2});
    }
  }

  @MinLenFieldInvariant(field = "minlen2", minLen = 4)
  class ValidSub extends Super {
    public final int[] validSubField;

    public ValidSub(int[] validSubField) {
      super(new int[] {1, 2, 3, 4});
      this.validSubField = validSubField;
    }
  }

  // :: error: (field.invariant.not.found.superclass)
  @MinLenFieldInvariant(field = "validSubField", minLen = 3)
  class InvalidSubSub1 extends ValidSub {
    public InvalidSubSub1() {
      super(new int[] {1, 2});
    }
  }

  // :: error: (field.invariant.not.subtype.superclass)
  @MinLenFieldInvariant(field = "minlen2", minLen = 3)
  class InvalidSubSub2 extends ValidSub {
    public InvalidSubSub2() {
      super(new int[] {1, 2});
    }
  }

  @FieldInvariant(field = "minlen2", qualifier = BottomVal.class)
  @MinLenFieldInvariant(field = "validSubField", minLen = 4)
  class ValidSubSub extends ValidSub {
    public ValidSubSub() {
      super(null);
    }

    void test() {
      int @BottomVal [] bot = minlen2;
      int @MinLen(4) [] four = validSubField;
    }
  }
}