checker/tests/calledmethods/Postconditions.java

import org.checkerframework.checker.calledmethods.qual.*;

/** Test for postcondition support via @EnsureCalledMethods. */
public class Postconditions {
  void build(@CalledMethods({"a", "b", "c"}) Postconditions this) {}

  void a() {}

  void b() {}

  void c() {}

  @EnsuresCalledMethods(value = "#1", methods = "b")
  static void callB(Postconditions x) {
    x.b();
  }

  @EnsuresCalledMethods(value = "#1", methods = "b")
  // :: error: contracts.postcondition
  static void doesNotCallB(Postconditions x) {}

  @EnsuresCalledMethods(
      value = "#1",
      methods = {"b", "c"})
  static void callBAndC(Postconditions x) {
    x.b();
    x.c();
  }

  static void allInOneMethod() {
    Postconditions y = new Postconditions();
    y.a();
    y.b();
    y.c();
    y.build();
  }

  static void invokeCallB() {
    Postconditions y = new Postconditions();
    y.a();
    callB(y);
    y.c();
    y.build();
  }

  static void invokeCallBLast() {
    Postconditions y = new Postconditions();
    y.a();
    y.c();
    callB(y);
    y.build();
  }

  static void invokeCallBAndC() {
    Postconditions y = new Postconditions();
    y.a();
    callBAndC(y);
    y.build();
  }

  static void invokeCallBAndCWrong() {
    Postconditions y = new Postconditions();
    callBAndC(y);
    // :: error: finalizer.invocation
    y.build();
  }

  @EnsuresCalledMethodsIf(
      expression = "#1",
      methods = {"a", "b", "c"},
      result = true)
  static boolean ensuresABCIfTrue(Postconditions p, boolean b) {
    if (b) {
      p.a();
      p.b();
      p.c();
      return true;
    }
    return false;
  }

  static void testEnsuresCalledMethodsIf(Postconditions p, boolean b) {
    if (ensuresABCIfTrue(p, b)) {
      p.build();
    } else {
      // :: error: finalizer.invocation
      p.build();
    }
  }

  @EnsuresCalledMethods(value = "#1", methods = "a")
  static void callWithException(Postconditions p) {
    try {
      p.a();
      throw new java.io.IOException();
    } catch (java.io.IOException e) {
    }
  }
}