checker/tests/nullness/EnsuresNonNullIfTest4.java

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

public class EnsuresNonNullIfTest4 {

  public void add_bottom_up(MyInvariant inv) {

    // The problem goes away if the below line is deleted or replaced with:
    //   Object x = new Object[100];
    Object x = new @Nullable Object[100];

    if (inv.is_ni_suppressed()) {
      Object ss = inv.get_ni_suppressions();
      ss.toString();
    }
  }
}

class MyInvariant {
  @Pure
  public @Nullable Object get_ni_suppressions() {
    return (null);
  }

  @SuppressWarnings("nullness")
  @EnsuresNonNullIf(result = true, expression = "get_ni_suppressions()")
  @Pure
  public boolean is_ni_suppressed() {
    return true;
  }
}