Package org.checkerframework.checker.calledmethods.qual

Annotation Interface EnsuresCalledMethods

@PostconditionAnnotation(qualifier=CalledMethods.class) @Target({METHOD,CONSTRUCTOR}) @Repeatable(List.class) public @interface EnsuresCalledMethods
Indicates that the method, if it terminates successfully, always invokes the given methods on the given expressions. This annotation is repeatable.

Consider the following method: 

 @EnsuresCalledMethods(value = "#1", methods = "m")
 public void callM(T t) { ... }

This method guarantees that t.m() is always called before the method returns.

If a class has any @Owning fields, then one or more of its must-call methods should be annotated to indicate that the must-call obligations are satisfied. The must-call methods are those named by the @MustCall or @InheritableMustCall annotation on the class declaration, such as close(). Here is a common example: 

 @EnsuresCalledMethods(value = {"owningField1", "owningField2"}, methods = "close")
 public void close() { ... }
See Also:
See the Checker Framework Manual:
Called Methods Checker

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static @interface 
    EnsuresCalledMethods.List
    A wrapper annotation that makes the EnsuresCalledMethods 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 to which the qualifier applies.

  • Element Details

    • value

      String[] value
      The Java expressions to which the qualifier applies.
      Returns:
      the Java expressions to which the qualifier applies
      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