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 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

public abstract 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

public abstract 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