org.checkerframework.framework.qual

Annotation Type EnsuresQualifier

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @InheritedAnnotation
 @Repeatable(value=EnsuresQualifier.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:

EnsuresQualifierIf

See the Checker Framework Manual:

Syntax of Java expressions

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	expression
Class<? extends Annotation>	qualifier

Element Detail

expression

public abstract String[] expression

Returns:

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

Returns:

the qualifier that is guaranteed to hold on successful termination of the method