import org.checkerframework.checker.nullness.qual.AssertNonNullIfNonNull;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;

// @skip-test Re-enable when @AssertNonNullIfNonNull checking is enhanced

public class AssertNonNullIfNonNullTest {

  private @Nullable String value;

  @Pure
  @AssertNonNullIfNonNull("value")
  public @Nullable String getValue() {
    return value;
  }

  public void setValue(String value) {
    this.value = value;
  }

  @EnsuresNonNullIf(expression = "value", result = true)
  public boolean isValueNonNull1() {
    return value != null;
  }

  @EnsuresNonNullIf(expression = "getValue()", result = true)
  public boolean isValueNonNull2() {
    // The @AssertNonNullIfNonNull annotation implies that if getValue() is
    // non-null, then is non-null, then value is non-null, but not the
    // converse, so an error should be issued here.
    // :: error: (contracts.conditional.postcondition)
    return value != null;
  }

  // The @AssertNonNullIfNonNull annotation should enable suppressing this error.
  @EnsuresNonNullIf(expression = "value", result = true)
  public boolean isValueNonNull3() {
    return getValue() != null;
  }

  @EnsuresNonNullIf(expression = "getValue()", result = true)
  public boolean isValueNonNull4() {
    return getValue() != null;
  }
}