org.checkerframework.checker.calledmethods.qual

Annotation Type EnsuresCalledMethods

@PostconditionAnnotation(qualifier=CalledMethods.class)
 @Target(value={METHOD,CONSTRUCTOR})
 @Repeatable(value=EnsuresCalledMethods.List.class)
public @interface EnsuresCalledMethods

Indicates that the method, if it terminates successfully, always invokes the given methods on the given expressions. This annotation is repeatable.

Consider the following method:

 @EnsuresCalledMethods(value = "#1", methods = "m")
 public void callM(T t) { ... }
 

This method guarantees that t.m() is always called before the method returns.

If a class has any @Owning fields, then one or more of its must-call methods should be annotated to indicate that the must-call obligations are satisfied. The must-call methods are those named by the @MustCall or @InheritableMustCall annotation on the class declaration, such as close(). Here is a common example:

 @EnsuresCalledMethods(value = {"owningField1", "owningField2"}, methods = "close")
 public void close() { ... }
 

See Also:

EnsuresCalledMethodsIf

See the Checker Framework Manual:

Called Methods Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	methods The methods guaranteed to be invoked on the expressions.
String[]	value The Java expressions to which the qualifier applies.

Element Detail

value

public abstract String[] value

The Java expressions to which the qualifier applies.

Returns:

the Java expressions to which the qualifier applies

See Also:

EnsuresQualifier

methods

@QualifierArgument(value="value")
public abstract String[] methods

The methods guaranteed to be invoked on the expressions.

Returns:

the methods guaranteed to be invoked on the expressions