checker/tests/nullness/AssertIfFalseTest2.java

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

public class AssertIfFalseTest2 {

  public static void usePriorityQueue(PriorityQueue1<@NonNull Object> active) {
    while (!(active.isEmpty())) {
      @NonNull Object queueMinPathNode = active.peek();
    }
  }

  ///////////////////////////////////////////////////////////////////////////
  /// Classes copied from the annotated JDK
  ///

  public class PriorityQueue1<E extends @NonNull Object> {
    @EnsuresNonNullIf(
        result = false,
        expression = {"peek()"})
    @Pure
    public boolean isEmpty() {
      return true;
    }

    @Pure
    public @Nullable E peek() {
      return null;
    }
  }
}