EnsuresLockHeldIf (checker-framework 3.39.0-eisop1 API)

```
@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:

EnsuresLockHeld

See the Checker Framework Manual:
Lock Checker, Example use of @EnsuresLockHeldIf

Required Element Summary

Required Elements
Modifier and Type	Required Element	Description
`java.lang.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 Detail
  - expression
```
java.lang.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:
    
    Syntax of Java expressions
- - 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