Nested and Inner Type Summary

Modifier and Type	Class and Description
public static @interface	EnsuresLockHeldIf.List A wrapper annotation that makes the `EnsuresLockHeldIf` annotation repeatable.

Method Summary

Modifier and Type	Method and Description
public String[]	Returns: Java expressions whose values are locks that are held after the method returns the given result expression() Returns Java expressions whose values are locks that are held after the method returns the given result.
public boolean	Returns: the return value of the method under which the postconditions hold result() Returns the return value of the method under which the postconditions hold.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

expression	back to summary
public String[] expression() Returns Java expressions whose values are locks that are held after the method returns the given result. Returns:String[] Java expressions whose values are locks that are held after the method returns the given result See Also Syntax of Java expressions

expression

back to summary

public String[] expression()

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

Returns:String[]: Java expressions whose values are locks that are held after the method returns the given result
See Also: Syntax of Java expressions

result	back to summary
public boolean result() Returns the return value of the method under which the postconditions hold. Returns:boolean the return value of the method under which the postconditions hold

result

back to summary

public boolean result()

Returns the return value of the method under which the postconditions hold.

Returns:boolean: the return value of the method under which the postconditions hold

org.checkerframework.checker.lock.qual back to summary

public @Interface EnsuresLockHeldIf.List

Annotations

extends Annotation

@Documented
@Retention:RUNTIME
@Target:METHOD, CONSTRUCTOR
@ConditionalPostconditionAnnotation
qualifier:LockHeld
@InheritedAnnotation

A wrapper annotation that makes the EnsuresLockHeldIf annotation repeatable.

Programmers generally do not need to write this. It is created by Java when a programmer writes more than one EnsuresLockHeldIf annotation at the same location.

Method Summary

Modifier and Type	Method and Description
public EnsuresLockHeldIf[]	Returns: the repeatable annotations value() Return the repeatable annotations.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

value	back to summary
public EnsuresLockHeldIf[] value() Return the repeatable annotations. Returns:EnsuresLockHeldIf[] the repeatable annotations

value

back to summary

public EnsuresLockHeldIf[] value()

Return the repeatable annotations.

Returns:EnsuresLockHeldIf[]: the repeatable annotations