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, which means that users can write more than one instance of it on the same method (users should NOT manually write an @EnsuresCalledMethods.List annotation, which the checker will create from multiple copies of this annotation automatically).

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 that will have methods called on them.

  • Element Details

    • value

      String[] value
      The Java expressions that will have methods called on them.
      Returns:
      the Java expressions that will have 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