Package org.checkerframework.framework.qual

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

    Nested Classes
    Modifier and Type
    Class
    Description
    static @interface 
    EnsuresQualifier.List
    A wrapper annotation that makes the EnsuresQualifier annotation repeatable.

  • Required Element Summary

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

  • Element Details

    • expression

      String[] expression
      Returns 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> qualifier
      Returns 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