org.checkerframework.checker.mustcall.qual

Annotation Type CreatesMustCallFor

@Target(value=METHOD)
 @InheritedAnnotation
 @Retention(value=RUNTIME)
 @Repeatable(value=CreatesMustCallFor.List.class)
public @interface CreatesMustCallFor

Indicates that the method resets the target's must-call type to its declared type. This effectively undoes flow-sensitive type refinement. The target is the value argument/element. More precisely, a call to a method annotated by this annotation changes the target's must-call type to the least upper bound of its current must-call type and its declared must-call type.

When calling a method annotated as @CreatesMustCallFor("target"), the expression target's static type in the Called Methods type system must be @CalledMethods({}). That is, target's CalledMethods type must be empty.

@CreatesMustCallFor("this") must be written on any method that assigns a non-final, owning field whose declared type has a must-call obligation.

This annotation is trusted, not checked. (Because this annotation can only add obligations, the analysis remains sound.)

For example, consider the following code, which uses a @CreatesMustCallFor annotation to indicate that the reset() method re-assigns the socket field:

 @MustCall("stop")
 class SocketContainer {
     // Note that @MustCall("close") is the default type for java.net.Socket, but it
     // is included on the next line for illustrative purposes. This example would function
     // identically if that qualifier were omitted.
     private @Owning @MustCall("close") Socket socket = ...;

     @EnsuresCalledMethods(value="this.socket", methods="close")
     public void stop() throws IOException {
       socket.close();
     }

    @CreatesMustCallFor("this")
    public void reset() {
      if (socket.isClosed()) {
        socket = new Socket(...);
      }
    }
 }
 

A client of SocketContainer is permitted to call reset() arbitrarily many times. Each time it does so, a new Socket might be created. A SocketContainer's must-call obligation of "stop" is fulfilled only if stop() is called after the last call to reset(). The @CreatesMustCallFor annotation on reset()'s declaration enforces this requirement: at any call to reset(), all called-methods information about the receiver is removed from the store of the Must Call Checker and the store of the Called Methods Checker, so the client has to "start over" as if a fresh SocketContainer object had been created.

When the -AnoCreatesMustCallFor command-line argument is passed to the checker, this annotation is ignored and all fields are treated as non-owning.

See the Checker Framework Manual:

Resource Leak Checker

Optional Element Summary

Optional Elements

Modifier and Type	Optional Element and Description
String	value The target of this annotation is stored in this field.

Element Detail

value

@JavaExpression
public abstract String value

The target of this annotation is stored in this field. The target must be an expression which can be refined in the store, such as a local variable or field.

Returns:

the expression to which must-call obligations are added when the annotated method is invoked

Default:

"this"