Package org.checkerframework.checker.lock.qual

Annotation Interface EnsuresLockHeldIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=LockHeld.class) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresLockHeldIf
Indicates that the given expressions are held if the method terminates successfully and returns the given result (either true or false).
See Also:
See the Checker Framework Manual:
Lock Checker, Example use of @EnsuresLockHeldIf

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
    Returns Java expressions whose values are locks that are held after the method returns the given result.
    boolean
    result
    Returns the return value of the method under which the postconditions hold.

  • Element Details

    • result

      boolean result
      Returns the return value of the method under which the postconditions hold.
      Returns:
      the return value of the method under which the postconditions hold

    • expression

      String[] expression
      Returns Java expressions whose values are locks that are held after the method returns the given result.
      Returns:
      Java expressions whose values are locks that are held after the method returns the given result
      See Also: