org.checkerframework.checker.lock.qual

Annotation Type EnsuresLockHeldIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @InheritedAnnotation
public @interface EnsuresLockHeldIf

Indicates that the given expressions are @LockHeld if the method returns the given result (either true or false).

See Also:

LockHeld, EnsuresLockHeld

See the Checker Framework Manual:

Lock Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	expression Java expression(s) that are LockHeld after the method returns the given result.
boolean	result The return value of the method that needs to hold for the postcondition to hold.

Element Detail

expression

public abstract String[] expression

Java expression(s) that are LockHeld after the method returns the given result.

See Also:

Syntax of Java expressions

result

public abstract boolean result

The return value of the method that needs to hold for the postcondition to hold.