The Checker Framework Manual:
Custom pluggable types for Java

Chapter 29 Must Call Checker

The Must Call Checker conservatively over-approximates the set of methods that an object should call before it is de-allocated. The checker does not enforce any rules other than subtyping; in particular, it does not enforce that the methods are called before objects are de-allocated. The Must Call Checker is intended to be run as a subchecker of another checker. The primary client of the Must Call Checker is the Resource Leak Checker (Chapter 8), which enforces that every method in a must-call obligation for an expression is called before that expression is de-allocated.

For example, consider a java.io.OutputStream. This OutputStream might have an obligation to call the close() method, to release an underlying file resource. The type of this OutputStream is @MustCall({"close"}). Or, the OutputStream might not have such an obligation, if the underlying resource is a byte array. The type of this OutputStream is @MustCall({}). For an arbitrary OutputStream, the Must Call Checker over-approximates the methods that it should call by assigning it the type @MustCall({"close"}) OutputStream, which can be read as “an OutputStream that might need to call close() (but no other methods) before it is de-allocated”.

If you are running the Resource Leak Checker (Chapter 8), then there is no need to run the Must Call Checker, because the Resource Leak Checker does so automatically. Running both may cause warning suppressions for the Must Call Checker not to work.

29.1 Must Call annotations

The Must Call Checker supports these type qualifiers:

@MustCall(String[] value)

gives a superset of the methods that must be called before the expression’s value is de-allocated. The annotation is not refined after a method is called; an expression of type @MustCall("foo") might or might not have already had foo() called on it. The default type qualifier for an unannotated type is @MustCall({}).

@MustCallUnknown

represents a value with an unknown or infinite set of must-call obligations. It is used internally by the type system but should never be written by a programmer.

@PolyMustCall

is the polymorphic annotation for the Must Call type system. For a description of polymorphic qualifiers, see Section 32.2.

@InheritableMustCall(String[] value)

is an alias of @MustCall that can only be written on a class declaration. It applies both to the class declaration on which it is written and also to all subclasses. This frees the user of the need to write the @MustCall annotation on every subclass. See Section 29.2 for details.

Here are some facts about the type qualifier hierarchy, which is shown in Figure 29.1. Any expression of type @MustCall({}) Object also has type @MustCall({"foo"}) Object. The type @MustCall({"foo"}) Object contains objects that need to call foo and objects that need to call nothing, but the type does not contain an object that needs to call bar (or both foo and bar). @MustCall({"foo", "bar"}) Object represents all objects that need to call foo, bar, both, or neither; it cannot represent an object that needs to call some other method.

29.2 Writing @MustCall/@InheritableMustCall on a class

As explained in Section 33.3, a type annotation on a type declaration means that every use of the type has that annotation by default. If a class A’s declaration has a @MustCall annotation, then A’s subclasses usually should too. To do so, a programmer can either write a @MustCall annotation on every subclass, or can write @InheritableMustCall on only A, which will cause the checker to treat every subclass as if it has an identical @MustCall annotation. The latter is the preferred style.

For example, given the following class annotation:

    package java.net;

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

    @InheritableMustCall({"close"}) class Socket { }

any use of Socket or a subclass of Socket defaults to @MustCall({"close"}) Socket.

The @InheritableMustCall annotation is necessary because type annotations cannot be made inheritable. @InheritableMustCall is a declaration annotation.

29.3 Relationship to lightweight ownership

The Must Call Checker interacts with the @Owning and @NotOwning annotations of the Resource Leak Checker (Chapter 8). In particular, any location that the Resource Leak Checker would consider “non-owning” (e.g., unannotated parameters and @NotOwning returns) is treated as @MustCall({}) by the Must Call Checker. This can lead to surprising results when running the Must Call Checker alone (which is not recommended). For example, consider the following program:

    @MustCall({"toString"}) String foo(@MustCall({"hashCode"}) String arg) {
      return arg;
    }

The Must Call Checker will not issue a warning about this code, because arg is non-owning (and therefore treated as @MustCall({})).

29.4 Assumptions about reflection

The Must Call Checker is unsound with respect to reflection: it assumes that objects instantiated reflectively do not have must-call obligations (i.e., that their type is @MustCall({})). If the checker is run with -AresolveReflection, then this assumption applies only to types that cannot be resolved.

29.5 Type parameter bounds often need to be annotated

In an unannotated program, there may be mismatches between defaulted type qualifiers that lead to type-checking errors. That is, the defaulted annotations at two different locations may be different and in conflict. A specific example is in code that contains a mix of explicit upper bounds with an extends clause and implicit upper bounds without an extends clause.

For example, consider the following example (from plume-util) of an interface with explicit upper bounds and a client with implicit upper bounds:

    interface Partitioner<ELEMENT extends @Nullable Object, CLASS extends @Nullable Object> {}

    class MultiRandSelector<T> {
      private Partitioner<T, T> eq;
    }

The code contains no @MustCall annotations. Running the Must Call Checker on this code produces an error at each use of T in MultiRandSelector:

error: [type.argument] incompatible type argument for type parameter ELEMENT of Partitioner.
        private Partitioner<T, T> eq;
                             ^
  found   : T extends @MustCallUnknown Object
  required: @MustCall Object
error: [type.argument] incompatible type argument for type parameter CLASS of Partitioner.
        private Partitioner<T, T> eq;
                               ^
  found   : T extends @MustCallUnknown Object
  required: @MustCall Object

The defaulted Must Call annotations differ. Partitioner has an explicit bound, which uses the usual default of @MustCall({}). MultiRandSelector has an implicit bound, which defaults to top (that is, @MustCallUnknown), as explained in Section 33.5.3.

In many cases, including this one, you can eliminate the false positive warning without writing any @MustCall annotations. You can either:

• • add an explicit bound to MultiRandSelector, changing its declaration to class MultiRandSelector<T extends Object>, or

• • remove the explicit bound from Partitioner, changing its declaration to interface Partitioner<ELEMENT, CLASS>.