org.checkerframework.checker.lock.qual

Annotation Type EnsuresLockHeld

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @PostconditionAnnotation(qualifier=LockHeld.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresLockHeld.List.class)
public @interface EnsuresLockHeld

Indicates that the given expressions are held if the method terminates successfully.

See Also:

EnsuresLockHeldIf

See the Checker Framework Manual:

Lock Checker, Example use of @EnsuresLockHeld

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	value Returns Java expressions whose values are locks that are held after successful method termination.

Element Detail

value

public abstract String[] value

Returns Java expressions whose values are locks that are held after successful method termination.

Returns:

Java expressions whose values are locks that are held after successful method termination

See Also:

Syntax of Java expressions