org.checkerframework.checker.lock.qual

Annotation Type EnsuresLockHeldIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=LockHeld.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresLockHeldIf.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 and Description
String[]	expression
boolean	result

Element Detail

expression

public abstract String[] expression

Returns:

Java expressions whose values are locks that are held after the method returns the given result

See Also:

Syntax of Java expressions

result

public abstract boolean result

Returns:

the return value of the method under which the postconditions hold