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

public class RequiresNonNullTest {

  @Nullable Object field1;
  @Nullable Object field2;

  @RequiresNonNull("field1")
  void method1() {
    field1.toString(); // OK, field1 is known to be non-null
    this.field1.toString(); // OK, field1 is known to be non-null
    // :: error: (dereference.of.nullable)
    field2.toString(); // error, might throw NullPointerException
  }

  @RequiresNonNull("field1")
  void method1also() {
    // ok, precondition satisfied by NNOE
    method1();
  }

  void method2() {
    field1 = new Object();
    method1(); // OK, satisfies method precondition
    field1 = null;
    // :: error: (contracts.precondition)
    method1(); // error, does not satisfy method precondition
  }

  protected @Nullable Object field;

  @RequiresNonNull("field")
  public void requiresNonNullField() {}

  public void clientFail(RequiresNonNullTest arg1) {
    // :: error: (contracts.precondition)
    arg1.requiresNonNullField();
  }

  public void clientOK(RequiresNonNullTest arg2) {
    arg2.field = new Object();
    // note that the following line works
    @NonNull Object o = arg2.field;

    arg2.requiresNonNullField(); // OK, field is known to be non-null
  }

  // TODO: forbid the field in @NNOE to be less visible than the method

  protected static @Nullable Object staticfield;

  @Pure
  @RequiresNonNull("staticfield")
  // :: warning: (purity.deterministic.void.method)
  public void reqStaticName() {
    reqStaticQualName();
  }

  @Pure
  @RequiresNonNull("RequiresNonNullTest.staticfield")
  // :: warning: (purity.deterministic.void.method)
  public void reqStaticQualName() {
    reqStaticName();
  }

  public void statClientOK(RequiresNonNullTest arg1) {
    staticfield = new Object();
    arg1.reqStaticName();

    staticfield = new Object();
    arg1.reqStaticQualName();

    RequiresNonNullTest.staticfield = new Object();
    arg1.reqStaticName();
    RequiresNonNullTest.staticfield = new Object();
    arg1.reqStaticQualName();
  }

  public void statClientFail(RequiresNonNullTest arg1) {
    // :: error: (contracts.precondition)
    arg1.reqStaticName();
    // :: error: (contracts.precondition)
    arg1.reqStaticQualName();
  }

  class NNOESubTest extends RequiresNonNullTest {
    public void subClientOK(NNOESubTest arg3) {
      arg3.field = new Object();
      arg3.requiresNonNullField();
    }

    public void subClientFail(NNOESubTest arg4) {
      // :: error: (contracts.precondition)
      arg4.requiresNonNullField();
    }

    public void subStat(NNOESubTest arg5) {
      RequiresNonNullTest.staticfield = new Object();
      arg5.reqStaticQualName();

      staticfield = new Object();
      arg5.reqStaticQualName();

      NNOESubTest.staticfield = new Object();
      arg5.reqStaticQualName();
    }
  }

  private @Nullable Object notHidden;

  class NNOEHidingTest extends RequiresNonNullTest {

    protected @Nullable String field;

    public void hidingClient1(NNOEHidingTest arg5) {
      arg5.field = "ha!";

      // TODO: The error message should say something about the hidden field.
      // :: error: (contracts.precondition)
      arg5.requiresNonNullField();

      // TODO: Add test like:
      // arg5.ensuresNonNullField();
      // arg5.requiresNonNullField();
    }

    public void hidingClient2(NNOEHidingTest arg6) {
      // :: error: (contracts.precondition)
      arg6.requiresNonNullField();
    }

    protected @Nullable Object notHidden;

    @RequiresNonNull("notHidden")
    void notHiddenTest() {
      // the field in the superclass is private -> don't complain about hiding
    }
  }

  static @Nullable Object o = "m";

  @RequiresNonNull("o")
  void test() {
    o = null;
  }

  @RequiresNonNull("thisShouldIssue1Error")
  // Test case for Issue 1051
  // https://github.com/typetools/checker-framework/issues/1051
  // :: error: (flowexpr.parse.error)
  void testIssue1051() {}
}