Nested and Inner Type Summary

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

Method Summary

Modifier and Type	Method and Description
public String[]	Returns: an array of Java expressions expression() Returns Java expressions that have had the given methods called on them after the method returns `result`.
public String[]	Returns: the methods guaranteed to be invoked on the expressions if the result of the method is `result` methods() The methods guaranteed to be invoked on the expressions if the result of the method is `result`.
public boolean	Returns: the return value of the method under which the postcondition holds result() Returns the return value of the method under which the postcondition holds.

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

Method Detail

expression back to summary

expression	back to summary
public String[] expression() Returns Java expressions that have had the given methods called on them after the method returns `result`. Returns:String[] an array of Java expressions

public String[] expression()

Returns Java expressions that have had the given methods called on them after the method returns result.

Returns:String[]: an array of Java expressions

methods back to summary

methods	back to summary
public String[] methods() The methods guaranteed to be invoked on the expressions if the result of the method is `result`. Returns:String[] the methods guaranteed to be invoked on the expressions if the result of the method is `result` Annotations @QualifierArgument:value

public String[] methods()

The methods guaranteed to be invoked on the expressions if the result of the method is result.

Returns:String[]

the methods guaranteed to be invoked on the expressions if the result of the method is result

Annotations

@QualifierArgument:value

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

result

back to summary

public boolean result()

Returns the return value of the method under which the postcondition holds.

Returns:boolean: the return value of the method under which the postcondition holds

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

public @Interface EnsuresCalledMethodsIf.List

Annotations

extends Annotation

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

A wrapper annotation that makes the EnsuresCalledMethodsIf annotation repeatable.

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

Method Summary

Modifier and Type	Method and Description
public EnsuresCalledMethodsIf[]	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 EnsuresCalledMethodsIf[] value() Return the repeatable annotations. Returns:EnsuresCalledMethodsIf[] the repeatable annotations

value

back to summary

public EnsuresCalledMethodsIf[] value()

Return the repeatable annotations.

Returns:EnsuresCalledMethodsIf[]: the repeatable annotations