checker/tests/nullness/Issue2013.java

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.dataflow.qual.Pure;

// @skip-test
public class Issue2013 {
  static class Super {
    private @Nullable String name = null;

    @EnsuresNonNull("name()")
    // :: error: (contracts.postcondition)
    void ensureNameNonNull() {
      name = "name";
    }

    @RequiresNonNull("name()")
    void requiresNameNonNull() {
      name().equals("name");
    }

    @Pure
    @Nullable String name() {
      return name;
    }
  }

  static class Sub extends Super {
    @Nullable String subname = null;

    @Override
    // :: error: (contracts.postcondition)
    void ensureNameNonNull() {
      super.ensureNameNonNull();
      subname = "Sub";
    }

    public static boolean flag;

    @Override
    @RequiresNonNull("name()")
    void requiresNameNonNull() {
      if (flag) {
        name().toString();
      } else {
        super.requiresNameNonNull();
      }
    }

    @Override
    @Nullable String name() {
      return subname;
    }

    void use() {
      if (super.name() != null) {
        // :: error: (contracts.precondition)
        requiresNameNonNull();
      }

      if (this.name() != null) {
        requiresNameNonNull();
      }

      if (super.name() != null) {
        // :: error: (contracts.precondition)
        super.requiresNameNonNull();
      }

      if (this.name() != null) {
        super.requiresNameNonNull();
      }

      super.ensureNameNonNull();
      // :: error: (contracts.precondition)
      requiresNameNonNull();

      super.ensureNameNonNull();
      // :: error: (contracts.precondition)
      super.requiresNameNonNull();

      ensureNameNonNull();
      super.requiresNameNonNull();

      ensureNameNonNull();
      requiresNameNonNull();
    }
  }

  void method(Super superObj) {
    if (superObj.name() != null) {
      superObj.requiresNameNonNull();
    }

    superObj.ensureNameNonNull();
    superObj.requiresNameNonNull();
  }

  void method2(Sub subObj) {
    if (subObj.name() != null) {
      subObj.requiresNameNonNull();
    }

    if (subObj.name() != null) {
      subObj.requiresNameNonNull();
    }
  }
}