checker/tests/nullness/NNOEStaticFields.java

import java.util.Collections;
import java.util.Set;
import org.checkerframework.checker.initialization.qual.*;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

public class NNOEStaticFields {
  static @Nullable String nullable = null;
  static @Nullable String otherNullable = null;

  @RequiresNonNull("nullable")
  void testF() {
    nullable.toString();
  }

  @RequiresNonNull("NNOEStaticFields.nullable")
  void testF2() {
    nullable.toString();
  }

  @RequiresNonNull("nullable")
  void testF3() {
    NNOEStaticFields.nullable.toString();
  }

  @RequiresNonNull("NNOEStaticFields.nullable")
  void testF4() {
    NNOEStaticFields.nullable.toString();
  }

  class Inner {
    void m1(NNOEStaticFields out) {
      NNOEStaticFields.nullable = "haha!";
      out.testF4();
    }

    @RequiresNonNull("NNOEStaticFields.nullable")
    void m2(NNOEStaticFields out) {
      out.testF4();
    }
  }

  @RequiresNonNull("NoClueWhatThisShouldBe")
  // :: error: (flowexpr.parse.error)
  void testF5() {
    // :: error: (dereference.of.nullable)
    NNOEStaticFields.nullable.toString();
  }

  void trueNegative() {
    // :: error: (dereference.of.nullable)
    nullable.toString();
    // :: error: (dereference.of.nullable)
    otherNullable.toString();
  }

  @RequiresNonNull("nullable")
  void test1() {
    nullable.toString();
    // :: error: (dereference.of.nullable)
    otherNullable.toString();
  }

  @RequiresNonNull("otherNullable")
  void test2() {
    // :: error: (dereference.of.nullable)
    nullable.toString();
    otherNullable.toString();
  }

  @RequiresNonNull({"nullable", "otherNullable"})
  void test3() {
    nullable.toString();
    otherNullable.toString();
  }

  @RequiresNonNull("System.out")
  void test4() {
    @NonNull Object f = System.out;
  }

  ///////////////////////////////////////////////////////////////////////////
  /// Copied from Daikon's ChicoryPremain
  ///

  static class ChicoryPremain1 {

    // Non-null if doPurity == true
    private static @MonotonicNonNull Set<String> pureMethods = null;

    private static boolean doPurity = false;

    @EnsuresNonNullIf(result = true, expression = "ChicoryPremain1.pureMethods")
    // this postcondition cannot be proved with the Checker Framework, as the relation
    // between doPurity and pureMethods is not explicit
    public static boolean shouldDoPurity() {
      // :: error: (contracts.conditional.postcondition)
      return doPurity;
    }

    @RequiresNonNull("ChicoryPremain1.pureMethods")
    public static Set<String> getPureMethods() {
      return Collections.unmodifiableSet(pureMethods);
    }
  }

  static class ClassInfo1 {
    public void initViaReflection() {
      if (ChicoryPremain1.shouldDoPurity()) {
        for (String pureMeth : ChicoryPremain1.getPureMethods()) {}
      }
    }
  }
}