import java.util.Map;
import org.checkerframework.checker.nullness.qual.*;

public class ParameterExpression {
  public void m1(
      @Nullable Object o, @Nullable Object o1, @Nullable Object o2, @Nullable Object o3) {
    // :: error: (flowexpr.parse.error.postcondition)
    m2(o);
    // :: error: (dereference.of.nullable)
    o.toString();
    m3(o);
    o.toString();
    m4(o1, o2, o3);
    // :: error: (dereference.of.nullable)
    o1.toString();
    // :: error: (dereference.of.nullable)
    o2.toString();
    o3.toString();
  }

  @SuppressWarnings("assert.postcondition")
  // "#0" is illegal syntax; it should be "#1"
  @EnsuresNonNull("#0")
  // :: error: (flowexpr.parse.error)
  public void m2(final @Nullable Object o) {}

  @SuppressWarnings("contracts.postcondition")
  @EnsuresNonNull("#1")
  public void m3(final @Nullable Object o) {}

  @SuppressWarnings("contracts.postcondition")
  @EnsuresNonNull("#3")
  public void m4(@Nullable Object x1, @Nullable Object x2, final @Nullable Object x3) {}

  // Formal parameter names should not be used in signatures (pre/postcondition, conditional
  // postcondition, and formal parameter annotations).  Use "#paramNum", because the parameter
  // names are not saved in bytecode.

  @Nullable Object field = null;

  // Postconditions
  @EnsuresNonNull("field") // OK
  public void m5() {
    field = new Object();
  }

  @EnsuresNonNull("param")
  // :: error: (flowexpr.parse.error)
  public void m6a(Object param) {
    param = new Object();
  }

  @EnsuresNonNull("param")
  // :: error: (flowexpr.parse.error)
  public void m6b(Object param) {
    // :: error: (assignment)
    param = null;
  }

  @EnsuresNonNull("param")
  // :: error: (flowexpr.parse.error)
  public void m6c(@Nullable Object param) {
    param = new Object();
  }

  @EnsuresNonNull("param")
  // :: error: (flowexpr.parse.error)
  public void m6d(@Nullable Object param) {
    param = null;
  }

  @EnsuresNonNull("param.toString()")
  // :: error: (flowexpr.parse.error)
  public void m6e(@Nullable Object param) {
    param = null;
  }

  @EnsuresNonNull("field")
  // :: error: (contracts.postcondition)
  // :: warning: (expression.parameter.name.shadows.field)
  public void m7a(Object field) {
    field = new Object();
  }

  @EnsuresNonNull("field")
  // :: error: (contracts.postcondition)
  // :: warning: (expression.parameter.name.shadows.field)
  public void m7b(Object field) {
    // :: error: (assignment)
    field = null;
  }

  @EnsuresNonNull("field")
  // :: error: (contracts.postcondition)
  // :: warning: (expression.parameter.name.shadows.field)
  public void m7c(@Nullable Object field) {
    field = new Object();
  }

  @EnsuresNonNull("field")
  // :: error: (contracts.postcondition)
  // :: warning: (expression.parameter.name.shadows.field)
  public void m7d(@Nullable Object field) {
    field = null;
  }

  // Preconditions
  @RequiresNonNull("field") // OK
  public void m8() {}

  @RequiresNonNull("param")
  // :: error: (flowexpr.parse.error)
  public void m9(Object param) {}

  // Warning issued. 'field' is a field, but in this case what matters is that it is the name of a
  // formal parameter.
  @RequiresNonNull("field")
  // :: warning: (expression.parameter.name.shadows.field)
  public void m10(Object field) {}

  // Conditional postconditions
  @EnsuresNonNullIf(result = true, expression = "field") // OK
  public boolean m11() {
    field = new Object();
    return true;
  }

  @EnsuresNonNullIf(result = true, expression = "param")
  // :: error: (flowexpr.parse.error)
  public boolean m12(Object param) {
    param = new Object();
    return true;
  }

  // Warning issued. 'field' is a field, but in this case what matters is that it is the name of a
  // formal parameter.
  @EnsuresNonNullIf(result = true, expression = "field")
  // :: warning: (expression.parameter.name.shadows.field)
  public boolean m13a(@Nullable Object field) {
    field = new Object();
    // :: error: (contracts.conditional.postcondition)
    return true;
  }

  @EnsuresNonNullIf(result = true, expression = "field")
  // :: warning: (expression.parameter.name.shadows.field)
  public boolean m13b(@Nullable Object field) {
    field = new Object();
    return false;
  }

  @EnsuresNonNullIf(result = true, expression = "field")
  // :: warning: (expression.parameter.name.shadows.field)
  public boolean m13c(@Nullable Object field) {
    field = null;
    // :: error: (contracts.conditional.postcondition)
    return true;
  }

  @EnsuresNonNullIf(result = true, expression = "field")
  // :: warning: (expression.parameter.name.shadows.field)
  public boolean m13d(@Nullable Object field) {
    field = null;
    return false;
  }

  // Annotations on formal parameters referring to a formal parameter of the same method.
  // :: error: (expression.unparsable)
  public void m14(@KeyFor("param2") Object param1, Map<Object, Object> param2) {}
}