checker/tests/mustcall/CreatesObligationSimple.java

// A simple test that @CreatesObligation works as intended wrt the Must Call Checker.

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

@MustCall("a") class CreatesObligationSimple {

  @CreatesObligation
  void reset() {}

  @CreatesObligation("this")
  void resetThis() {}

  static @MustCall({}) CreatesObligationSimple makeNoMC() {
    return null;
  }

  static void test1() {
    CreatesObligationSimple cos = makeNoMC();
    @MustCall({}) CreatesObligationSimple a = cos;
    cos.reset();
    // :: error: assignment
    @MustCall({}) CreatesObligationSimple b = cos;
    @MustCall("a") CreatesObligationSimple c = cos;
  }

  static void test2() {
    CreatesObligationSimple cos = makeNoMC();
    @MustCall({}) CreatesObligationSimple a = cos;
    cos.resetThis();
    // :: error: assignment
    @MustCall({}) CreatesObligationSimple b = cos;
    @MustCall("a") CreatesObligationSimple c = cos;
  }

  static void test3() {
    Object cos = makeNoMC();
    @MustCall({}) Object a = cos;
    // :: error: createsobligation.target.unparseable
    ((CreatesObligationSimple) cos).reset();
    // It would be better to issue an assignment incompatible error here, but the
    // error above is okay too.
    @MustCall({}) Object b = cos;
    @MustCall("a") Object c = cos;
  }

  // Rewrite of test3 that follows the instructions in the error message.
  static void test4() {
    Object cos = makeNoMC();
    @MustCall({}) Object a = cos;
    CreatesObligationSimple r = ((CreatesObligationSimple) cos);
    r.reset();
    // :: error: assignment
    @MustCall({}) Object b = r;
    @MustCall("a") Object c = r;
  }
}