checker/tests/nullness/Issue2470.java

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

public class Issue2470 {
  static class Example {
    @MonotonicNonNull String s;

    public Example() {}

    @EnsuresNonNull("this.s")
    public Example setS(String s1) {
      this.s = s1;
      return this;
    }

    // TODO: Support "return" in Java Expression syntax.
    // @EnsuresNonNull("return.s")
    @EnsuresNonNull("this.s")
    public Example setS2(String s1) {
      this.s = s1;
      return this;
    }

    @RequiresNonNull("this.s")
    public void print() {
      System.out.println(this.s.toString());
    }
  }

  static void buggy() {
    new Example()
        // :: error: (contracts.precondition)
        .print();
  }

  static void ok() {
    Example e = new Example();
    e.setS("test");
    e.print();
  }

  static void buggy2() {
    new Example()
        .setS("test")
        // :: error:(contracts.precondition)
        .print();
  }

  // TODO: These should be legal, once "return" is supported in Java Expression syntax.
  // of a method.
  /*
  static void ok3() {
      Example e = new Example().setS2("test");
      e.print();
  }

  static void ok2() {
      new Example().setS2("test").print();
  }
  */
}