org.checkerframework.checker.mustcall.qual

Annotation Type CreatesObligation

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

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, the method resets 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 @CreatesObligation("target"), the expression target must not have type @CalledMethods({}). That is, target's CalledMethods type must be non-empty.

@CreatesObligation("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 @CreatesObligation 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();
     }

    @CreatesObligation("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 @CreatesObligation 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 -AnoCreatesObligation 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:

Must Call 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"