Package org.checkerframework.checker.calledmethods.qual

Annotation Interface EnsuresCalledMethodsOnException

@Target({METHOD,CONSTRUCTOR}) @Repeatable(List.class) @Retention(RUNTIME) @InheritedAnnotation public @interface EnsuresCalledMethodsOnException
Indicates that the method, if it terminates by throwing an Exception, 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 @EnsuresCalledMethodsOnException.List annotation, which the checker will create from multiple copies of this annotation automatically).

Consider the following method: 

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

The callM method promises to always call t.m() before throwing any kind of Exception.

Note that EnsuresCalledMethodsOnException only describes behavior for Exception (and by extension RuntimeException, NullPointerException, etc.) but not Error or other throwables.

See Also:
See the Checker Framework Manual:
Called Methods Checker

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    methods
    The methods guaranteed to be invoked on the expressions if the result of the method throws an exception.
    String[]
    value
    Returns Java expressions that have had the given methods called on them after the method throws an exception.

  • Element Details

    • value

      String[] value
      Returns Java expressions that have had the given methods called on them after the method throws an exception.
      Returns:
      an array of Java expressions
      See the Checker Framework Manual:
      Syntax of Java expressions

    • methods

      String[] methods
      The methods guaranteed to be invoked on the expressions if the result of the method throws an exception.
      Returns:
      the methods guaranteed to be invoked on the expressions if the method throws an exception