@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() { ... }
EnsuresCalledMethodsIf
| Modifier and Type | Class and Description |
|---|---|
| public static @interface | EnsuresCalledMethods.List
A wrapper annotation that makes the |
| Modifier and Type | Method and Description |
|---|---|
| public String[] | Returns: the methods guaranteed to be invoked on the expressionsThe methods guaranteed to be invoked on the expressions. |
| public String[] | Returns: the Java expressions to which the qualifier appliesThe Java expressions to which the qualifier applies. |
| methods | back to summary |
|---|---|
| public String[] methods() The methods guaranteed to be invoked on the expressions.
| |
| value | back to summary |
|---|---|
| public String[] value() The Java expressions to which the qualifier applies.
| |
EnsuresCalledMethods annotation repeatable. This
annotation is an implementation detail: programmers generally do not need to write this. It is
created automatically by Java when a programmer writes more than one EnsuresCalledMethods annotation at the same location.
| Modifier and Type | Method and Description |
|---|---|
| public EnsuresCalledMethods[] |
| value | back to summary |
|---|---|
| public EnsuresCalledMethods[] value() Return the repeatable annotations.
| |