Package org.checkerframework.checker.lock.qual

Annotation Interface EnsuresLockHeld

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @PostconditionAnnotation(qualifier=LockHeld.class) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresLockHeld
Indicates that the given expressions are held if the method terminates successfully.
See Also:
See the Checker Framework Manual:
Lock Checker, Example use of @EnsuresLockHeld

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    value
    Returns Java expressions whose values are locks that are held after successful method termination.

  • Element Details

    • value

      String[] value
      Returns Java expressions whose values are locks that are held after successful method termination.
      Returns:
      Java expressions whose values are locks that are held after successful method termination
      See Also: