EnsuresCalledMethods (checker-framework 3.39.0-eisop1 API)

```
@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:

EnsuresCalledMethodsIf

See the Checker Framework Manual:
Called Methods Checker

Required Element Summary

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

- Element Detail
  - value
```
java.lang.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:
    
    EnsuresQualifier
- - methods
```
@QualifierArgument("value")
java.lang.String[] methods
```
    The methods guaranteed to be invoked on the expressions.
    
    Returns:
    
    the methods guaranteed to be invoked on the expressions