Annotation Interface EnsuresQualifier
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@InheritedAnnotation
@Repeatable(List.class)
public @interface EnsuresQualifier
A postcondition annotation to indicate that a method ensures that certain expressions have a
certain type qualifier once the method has successfully terminated. The expressions for which the
qualifier holds after the method's execution are indicated by
expression
and are
specified using a string. The qualifier is specified by the qualifier
annotation element.
Here is an example use:
@EnsuresQualifier(expression = "p.f1", qualifier = Odd.class)
void oddF1_1() {
p.f1 = null;
}
Some type systems have specialized versions of this annotation, such as
org.checkerframework.checker.nullness.qual.EnsuresNonNull
and
org.checkerframework.checker.lock.qual.EnsuresLockHeld
.- See Also:
- See the Checker Framework Manual:
- Syntax of Java expressions
-
Nested Class Summary
Modifier and TypeClassDescriptionstatic @interface
A wrapper annotation that makes theEnsuresQualifier
annotation repeatable. -
Required Element Summary
Modifier and TypeRequired ElementDescriptionString[]
Returns the Java expressions for which the qualifier holds after successful method termination.Class<? extends Annotation>
Returns the qualifier that is guaranteed to hold on successful termination of the method.
-
Element Details
-
expression
String[] expressionReturns the Java expressions for which the qualifier holds after successful method termination.- Returns:
- the Java expressions for which the qualifier holds after successful method termination
- See the Checker Framework Manual:
- Syntax of Java expressions
-
qualifier
Class<? extends Annotation> qualifierReturns the qualifier that is guaranteed to hold on successful termination of the method.- Returns:
- the qualifier that is guaranteed to hold on successful termination of the method
-