org.checkerframework.checker.lock.qual

Annotation Type EnsuresLockHeldIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=LockHeld.class)
 @InheritedAnnotation
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 Java expressions whose values are held 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 expressions whose values are held 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.