Package org.checkerframework.checker.calledmethods.qual

Annotation Interface RequiresCalledMethods

@Documented @Retention(RUNTIME) @PreconditionAnnotation(qualifier=CalledMethods.class) @Target({METHOD,CONSTRUCTOR}) @Repeatable(List.class) public @interface RequiresCalledMethods
Indicates a method precondition: when the method is invoked, the specified expressions must have had the specified methods called on them.

Do not use this annotation for formal parameters; instead, give their type a @CalledMethods annotation. The @RequiresCalledMethods annotation is intended for other expressions, such as field accesses or method calls.

See the Checker Framework Manual:
Called Methods Checker

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    methods
    The methods guaranteed to be invoked on the expressions.
    String[]
    value
    The Java expressions that must have had methods called on them.

  • Element Details

    • value

      String[] value
      The Java expressions that must have had methods called on them.
      Returns:
      the Java expressions that must have had methods called on them
      See Also:

    • methods

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