// Test case for Issue 391:
// https://github.com/typetools/checker-framework/issues/391

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

class ClassA {
  private @Nullable String value = null;

  @EnsuresNonNull("value")
  public void ensuresNonNull() {
    value = "";
  }

  @RequiresNonNull("value")
  public String getValue() {
    return value;
  }
}

public class Issue391 {
  ClassA field = new ClassA();

  @RequiresNonNull("field.value")
  void method() {}

  @EnsuresNonNull("field.value")
  void ensuresNonNull() {
    field.ensuresNonNull();
  }

  void method2() {
    ClassA a = new ClassA();
    // :: error: (contracts.precondition)
    a.getValue();
    // :: error: (contracts.precondition)
    method();
  }

  void method3() {
    ensuresNonNull();
    method();

    ClassA a = new ClassA();
    a.ensuresNonNull();
    a.getValue();
  }
}