checker/tests/nullness/AssertNonNullTest.java

import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;

public class AssertNonNullTest {
  public @Nullable String s;

  // :: error: (contracts.postcondition)
  public @EnsuresNonNull("s") void makeNN() {
    s = null;
  }

  public static void main(String[] args) {
    AssertNonNullTest a = new AssertNonNullTest();
    // :: error: (dereference.of.nullable)
    a.s.equals("we");
    AssertNonNullTest b = new AssertNonNullTest();
    b.makeNN();
    b.s.equals("we");
  }
}