framework/tests/value/RepeatMinLenIfWithError.java

import org.checkerframework.common.value.qual.EnsuresMinLenIf;

public class RepeatMinLenIfWithError {

  protected String a;
  protected String b;
  protected String c;

  public boolean func1() {
    a = "checker";
    c = "framework";
    b = "hello";
    return true;
  }

  @EnsuresMinLenIf(
      expression = {"a", "b"},
      targetValue = 6,
      result = true)
  @EnsuresMinLenIf(expression = "c", targetValue = 6, result = true)
  public boolean client1() {
    return withcondpostconditionsfunc1();
  }

  @EnsuresMinLenIf.List({
    @EnsuresMinLenIf(expression = "a", targetValue = 6, result = true),
    @EnsuresMinLenIf(expression = "b", targetValue = 6, result = true)
  })
  @EnsuresMinLenIf(expression = "c", targetValue = 6, result = true)
  public boolean client2() {
    return withcondpostconditionfunc1();
  }

  @EnsuresMinLenIf(
      expression = {"a", "b"},
      targetValue = 6,
      result = true)
  @EnsuresMinLenIf(expression = "c", targetValue = 6, result = true)
  public boolean withcondpostconditionsfunc1() {
    a = "checker";
    c = "framework";
    b = "hello"; // condition not satisfied here
    // :: error:  (contracts.conditional.postcondition)
    return true;
  }

  @EnsuresMinLenIf.List({
    @EnsuresMinLenIf(expression = "a", targetValue = 6, result = true),
    @EnsuresMinLenIf(expression = "b", targetValue = 6, result = true)
  })
  @EnsuresMinLenIf(expression = "c", targetValue = 6, result = true)
  public boolean withcondpostconditionfunc1() {
    a = "checker";
    c = "framework";
    b = "hello"; // condition not satisfied here
    // :: error:  (contracts.conditional.postcondition)
    return true;
  }
}