EnsuresLockHeld (checker-framework 3.39.0-eisop1 API)

@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:: EnsuresLockHeldIf
See the Checker Framework Manual:: Lock Checker, Example use of @EnsuresLockHeld

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

- Element Detail
  - value
```
java.lang.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:
    
    Syntax of Java expressions