checker/tests/nullness/RepeatEnsuresKeyForWithError.java

import java.util.HashMap;
import java.util.Map;
import org.checkerframework.checker.nullness.qual.EnsuresKeyFor;
import org.checkerframework.checker.nullness.qual.EnsuresKeyForIf;

public class RepeatEnsuresKeyForWithError {

  Map<String, Integer> map = new HashMap<>();

  public void func1(String a, String b, String c) {
    map.put(a, 1);
    map.put(c, 3);
  }

  public boolean func2(String a, String b, String c) {
    map.put(a, 1);
    map.put(c, 3);
    return true;
  }

  @EnsuresKeyFor(
      value = {"#1", "#2"},
      map = "map")
  @EnsuresKeyFor(value = "#3", map = "map")
  public void client1(String a, String b, String c) {
    withpostconditionsfunc1(a, b, c);
  }

  @EnsuresKeyFor(
      value = {"#1", "#2"},
      map = "map")
  @EnsuresKeyFor(value = "#3", map = "map")
  public void client2(String a, String b, String c) {
    withpostconditionfunc1(a, b, c);
  }

  @EnsuresKeyForIf(
      expression = {"#1", "#2"},
      map = "map",
      result = true)
  @EnsuresKeyForIf(expression = "#3", map = "map", result = true)
  public boolean client3(String a, String b, String c) {
    return withcondpostconditionsfunc2(a, b, c);
  }

  @EnsuresKeyForIf.List({
    @EnsuresKeyForIf(expression = "#1", map = "map", result = true),
    @EnsuresKeyForIf(expression = "#2", map = "map", result = true)
  })
  @EnsuresKeyForIf(expression = "#3", map = "map", result = true)
  public boolean client4(String a, String b, String c) {
    return withcondpostconditionfunc2(a, b, c);
  }

  @EnsuresKeyFor(
      value = {"#1", "#2"},
      map = "map")
  @EnsuresKeyFor(value = "#3", map = "map")
  // :: error:  (contracts.postcondition)
  public void withpostconditionsfunc1(String a, String b, String c) {
    map.put(a, 1);
    map.put(c, 3);
  }

  @EnsuresKeyForIf(
      expression = {"#1", "#2"},
      map = "map",
      result = true)
  @EnsuresKeyForIf(expression = "#3", map = "map", result = true)
  public boolean withcondpostconditionsfunc2(String a, String b, String c) {
    map.put(a, 1);
    map.put(c, 3);
    // :: error:  (contracts.conditional.postcondition)
    return true;
  }

  @EnsuresKeyFor.List({
    @EnsuresKeyFor(value = "#1", map = "map"),
    @EnsuresKeyFor(value = "#2", map = "map"),
  })
  @EnsuresKeyFor(value = "#3", map = "map")
  // :: error:  (contracts.postcondition)
  public void withpostconditionfunc1(String a, String b, String c) {
    map.put(a, 1);
    map.put(c, 3);
  }

  @EnsuresKeyForIf.List({
    @EnsuresKeyForIf(expression = "#1", map = "map", result = true),
    @EnsuresKeyForIf(expression = "#2", map = "map", result = true)
  })
  @EnsuresKeyForIf(expression = "#3", map = "map", result = true)
  public boolean withcondpostconditionfunc2(String a, String b, String c) {
    map.put(a, 1);
    map.put(c, 3);
    // :: error:  (contracts.conditional.postcondition)
    return true;
  }
}