org.checkerframework.framework.qual

Annotation Type EnsuresQualifier

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @InheritedAnnotation
 @Repeatable(value=EnsuresQualifiers.class)
public @interface EnsuresQualifier

A postcondition annotation to indicate that a method ensures certain expressions to have a certain type qualifier once the method has successfully terminated. The expressions for which the qualifier must hold after the method's execution are indicated by expression and are specified using a string. The qualifier is specified by qualifier.

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:

EnsuresQualifierIf

See the Checker Framework Manual:

Syntax of Java expressions

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	expression The Java expressions for which the qualifier holds after successful method termination.
Class<? extends Annotation>	qualifier The qualifier that is guaranteed to hold on successfull termination of the method.

Element Detail

expression

public abstract String[] expression

The Java expressions for which the qualifier holds after successful method termination.

See the Checker Framework Manual:

Syntax of Java expressions

qualifier

public abstract Class<? extends Annotation> qualifier

The qualifier that is guaranteed to hold on successfull termination of the method.