org.checkerframework.checker.calledmethods.qual

Annotation Type RequiresCalledMethods

@Documented
 @Retention(value=RUNTIME)
 @PreconditionAnnotation(qualifier=CalledMethods.class)
 @Target(value={METHOD,CONSTRUCTOR})
public @interface RequiresCalledMethods

Indicates a method precondition: when the method is invoked, the specified expressions must have had the specified methods called on them.

Do not use this annotation for formal parameters; instead, give their type a @CalledMethods annotation. The @RequiresCalledMethods annotation is intended for other expressions, such as field accesses or method calls.

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 that must have had methods called on them.

Element Detail

value

public abstract String[] value

The Java expressions that must have had methods called on them.

Returns:

the Java expressions that must have had methods called on them

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