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

public class AssertAfterChecked {

  class InitField {
    @Nullable Object f;

    @EnsuresNonNull("f")
    void init() {
      f = new Object();
    }

    @EnsuresNonNull("f")
    // :: error: (contracts.postcondition)
    void initBad() {}

    void testInit() {
      init();
      f.toString();
    }
  }

  static class InitStaticField {
    static @Nullable Object f;

    @EnsuresNonNull("f")
    void init() {
      f = new Object();
    }

    @EnsuresNonNull("f")
    void init2() {
      InitStaticField.f = new Object();
    }

    @EnsuresNonNull("f")
    // :: error: (contracts.postcondition)
    void initBad() {}

    void testInit() {
      init();
      f.toString();
    }

    @EnsuresNonNull("InitStaticField.f")
    void initE() {
      f = new Object();
    }

    @EnsuresNonNull("InitStaticField.f")
    void initE2() {
      InitStaticField.f = new Object();
    }

    @EnsuresNonNull("InitStaticField.f")
    // :: error: (contracts.postcondition)
    void initBadE() {}

    void testInitE() {
      initE();
      // TODO: we need to also support the unqualified static field access?
      // f.toString();
    }

    void testInitE2() {
      initE();
      InitStaticField.f.toString();
    }
  }

  class TestParams {
    @EnsuresNonNull("get(#1)")
    // :: error: (contracts.postcondition)
    void init(final TestParams p) {}

    @org.checkerframework.dataflow.qual.Pure
    @Nullable Object get(Object o) {
      return null;
    }

    void testInit1() {
      init(this);
      get(this).toString();
    }

    void testInit1b() {
      init(this);
      this.get(this).toString();
    }

    void testInit2(TestParams p) {
      init(p);
      get(p).toString();
    }

    void testInit3(TestParams p) {
      p.init(this);
      p.get(this).toString();
    }

    void testInit4(TestParams p) {
      p.init(this);
      // :: error: (dereference.of.nullable)
      this.get(this).toString();
    }
  }

  class WithReturn {
    @Nullable Object f;

    @EnsuresNonNull("f")
    int init1() {
      f = new Object();
      return 0;
    }

    @EnsuresNonNull("f")
    int init2() {
      if (5 == 5) {
        f = new Object();
        return 0;
      } else {
        f = new Object();
        return 1;
      }
    }

    @EnsuresNonNull("f")
    // :: error: (contracts.postcondition)
    int initBad1() {
      return 0;
    }

    @EnsuresNonNull("f")
    // :: error: (contracts.postcondition)
    int initBad2() {
      if (5 == 5) {
        return 0;
      } else {
        f = new Object();
        return 1;
      }
    }

    void testInit() {
      init1();
      f.toString();
    }
  }
}