checker/tests/nullness/NullnessFieldInvar.java

package fieldinvar;

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.framework.qual.FieldInvariant;

public class NullnessFieldInvar {
  public class Super {
    public final @Nullable Object o;
    public @Nullable Object nonfinal = null;

    public Super(@Nullable Object o) {
      this.o = o;
    }
  }

  @FieldInvariant(field = "o", qualifier = NonNull.class)
  class Sub extends Super {
    public final @Nullable Object subO;

    public Sub(@NonNull Object o) {
      super(o);
      subO = null;
    }

    public Sub(@NonNull Object o, @Nullable Object subO) {
      super(o);
      this.subO = subO;
    }

    void test() {
      @NonNull Object x1 = this.o;
      @NonNull Object x2 = o;
      @NonNull Object x3 = super.o;
    }
  }

  class SubSub1 extends Sub {
    public SubSub1(@NonNull Object o) {
      super(o);
    }
  }

  @FieldInvariant(
      field = {"o", "subO"},
      qualifier = NonNull.class)
  class SubSub2 extends Sub {
    public SubSub2(@NonNull Object o) {
      super(o);
    }
  }

  class Use {
    void test(Super superO, Sub sub, SubSub1 subSub1, SubSub2 subSub2) {
      // :: error: (assignment)
      @NonNull Object x1 = superO.o;
      @NonNull Object x2 = sub.o;
      @NonNull Object x3 = subSub1.o;

      // :: error: (assignment)
      @NonNull Object x5 = sub.subO;
      // :: error: (assignment)
      @NonNull Object x6 = subSub1.subO;
      @NonNull Object x7 = subSub2.subO;
    }

    <SP extends Super, SB extends Sub, SS1 extends SubSub1, SS2 extends SubSub2> void test2(
        SP superO, SB sub, SS1 subSub1, SS2 subSub2) {
      // :: error: (assignment)
      @NonNull Object x1 = superO.o;
      @NonNull Object x2 = sub.o;
      @NonNull Object x3 = subSub1.o;

      // :: error: (assignment)
      @NonNull Object x5 = sub.subO;
      // :: error: (assignment)
      @NonNull Object x6 = subSub1.subO;
      @NonNull Object x7 = subSub2.subO;
    }
  }

  class SuperWithNonFinal {
    @Nullable Object nonfinal = null;
  }
  // nonfinal isn't final
  // :: error: (field.invariant.not.final)
  @FieldInvariant(field = "nonfinal", qualifier = NonNull.class)
  class SubSubInvalid extends SuperWithNonFinal {}

  // field is declared in this class
  // :: error: (field.invariant.not.found)
  @FieldInvariant(field = "field", qualifier = NonNull.class)
  class Invalid {
    final Object field = new Object();
  }

  @FieldInvariant(
      field = {"o", "subO"},
      qualifier = NonNull.class)
  class Shadowing extends SubSub2 {
    @Nullable Object o;
    @Nullable Object subO;

    void test() {
      // :: error: (assignment)
      @NonNull Object x = o; // error
      // :: error: (assignment)
      @NonNull Object x2 = subO; // error

      @NonNull Object x3 = super.o;
      @NonNull Object x4 = super.subO;
    }

    public Shadowing() {
      super("");
    }
  }

  // inherits: @FieldInvariant(field = {"o", "subO"}, qualifier = NonNull.class)
  class Inherits extends SubSub2 {
    @Nullable Object o;
    @Nullable Object subO;

    void test() {
      // :: error: (assignment)
      @NonNull Object x = o; // error
      // :: error: (assignment)
      @NonNull Object x2 = subO; // error

      @NonNull Object x3 = super.o;
      @NonNull Object x4 = super.subO;
    }

    public Inherits() {
      super("");
    }
  }

  class Super2 {}

  // :: error: (field.invariant.not.wellformed)
  @FieldInvariant(
      field = {},
      qualifier = NonNull.class)
  class Invalid1 extends Super2 {}
  // :: error: (field.invariant.not.wellformed)
  @FieldInvariant(
      field = {"a", "b"},
      qualifier = {NonNull.class, NonNull.class, NonNull.class})
  class Invalid2 extends Super2 {}

  // :: error: (field.invariant.not.found)
  @FieldInvariant(field = "x", qualifier = NonNull.class)
  class NoSuper {}

  class SuperManyFields {
    public final @Nullable Object field1 = null;
    public final @Nullable Object field2 = null;
    public final @Nullable Object field3 = null;
    public final @Nullable Object field4 = null;
  }

  @FieldInvariant(
      field = {"field1", "field2", "field3", "field4"},
      qualifier = NonNull.class)
  class SubManyFields extends SuperManyFields {
    void test() {
      field1.toString();
      field2.toString();
      field3.toString();
      field4.toString();
    }
  }
}