checker/tests/nullness/Issue1096.java

// Test case for Issue 1096:
// https://github.com/typetools/checker-framework/issues/1027

import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

class PreCond {
  Object f;
  @Nullable Object g;

  PreCond() {
    f = new Object();
    early();
    g = new Object();
    doNullable();
  }

  void earlyBad(@UnknownInitialization PreCond this) {
    // :: error: (dereference.of.nullable)
    f.toString();
  }

  @RequiresNonNull("this.f")
  void early(@UnknownInitialization PreCond this) {
    f.toString();
  }

  @RequiresNonNull("this.g")
  void doNullable(@UnknownInitialization PreCond this) {
    g.toString();
  }

  void foo(@UnknownInitialization PreCond this) {
    // The receiver is not fully initialized, so raise an error.
    // :: error: (contracts.precondition)
    early();
  }

  void bar() {
    // The receiver is initialized, so non-null field f is definitely non-null.
    early();
    // Nullable fields stay nullable
    // :: error: (contracts.precondition)
    doNullable();
  }
}

class User {
  void foo(@UnknownInitialization PreCond pc) {
    // The receiver is not fully initialized, so raise an error.
    // :: error: (contracts.precondition)
    pc.early();
  }

  void bar(PreCond pc) {
    // The receiver is initialized, so non-null field f is definitely non-null.
    pc.early();
    // Nullable fields stay nullable
    // :: error: (contracts.precondition)
    pc.doNullable();
  }
}