org.checkerframework.checker.calledmethods.qual

Annotation Type EnsuresCalledMethodsIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=CalledMethods.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresCalledMethodsIf.List.class)
public @interface EnsuresCalledMethodsIf

Indicates that the method, if it terminates with the given result, invokes the given methods on the given expressions.

See Also:

EnsuresCalledMethods, CalledMethods

See the Checker Framework Manual:

Called Methods Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	expression Returns Java expressions that have had the given methods called on them after the method returns result().
String[]	methods The methods guaranteed to be invoked on the expressions if the result of the method is result().
boolean	result Returns the return value of the method under which the postcondition holds.

Element Detail

expression

public abstract String[] expression

Returns Java expressions that have had the given methods called on them after the method returns result().

Returns:

an array of Java expressions

See the Checker Framework Manual:

Syntax of Java expressions

result

public abstract boolean result

Returns the return value of the method under which the postcondition holds.

Returns:

the return value of the method under which the postcondition holds

methods

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

The methods guaranteed to be invoked on the expressions if the result of the method is result().

Returns:

the methods guaranteed to be invoked on the expressions if the result of the method is result()