Package org.checkerframework.checker.calledmethods.qual

Annotation Interface EnsuresCalledMethodsIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=CalledMethods.class) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresCalledMethodsIf
Indicates that the method, if it terminates with the given result, invokes the given methods on the given expressions.
See Also:
See the Checker Framework Manual:
Called Methods Checker

  • Nested Class Summary

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

  • Required Element Summary

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

  • Element Details

    • expression

      String[] expression
      Returns Java expressions that have had the given methods called on them after the method returns result().
      Returns:
      an array of Java expressions
      See the Checker Framework Manual:
      Syntax of Java expressions

    • result

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

    • methods

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