Annotation Interface EnsuresNonNullIf
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@ConditionalPostconditionAnnotation(qualifier=NonNull.class)
@InheritedAnnotation
@Repeatable(List.class)
public @interface EnsuresNonNullIf
Indicates that the given expressions are non-null, if the method returns the given result (either
true or false).
Here are ways this conditional postcondition annotation can be used:
Method parameters: A common example is that the equals
method is annotated as
follows:
@EnsuresNonNullIf(expression="#1", result=true)
public boolean equals(@Nullable Object obj) { ... }
because, if equals
returns true, then the first (#1) argument to equals
was not
null.
Fields: The value expressions can refer to fields, even private ones. For example:
@EnsuresNonNullIf(expression="this.derived", result=true)
public boolean isDerived() {
return (this.derived != null);
}
As another example, an Iterator
may cache the next value that will be returned, in which
case its hasNext
method could be annotated as:
@EnsuresNonNullIf(expression="next_cache", result=true)
public boolean hasNext() {
if (next_cache == null) {
return false;
}
...
}
An EnsuresNonNullIf
annotation that refers to a private field is useful for verifying
that client code performs needed checks in the right order, even if the client code cannot
directly affect the field.
Method calls: If Class.isArray()
returns true, then Class.getComponentType()
returns non-null. You can express this relationship as:
@EnsuresNonNullIf(expression="getComponentType()", result=true)
public native @Pure boolean isArray();
You can write two @EnsuresNonNullIf
annotations on a single method:
@EnsuresNonNullIf(expression="outputFile", result=true)
@EnsuresNonNullIf(expression="memoryOutputStream", result=false)
public boolean isThresholdExceeded() { ... }
- See Also:
- See the Checker Framework Manual:
- Nullness Checker
-
Nested Class Summary
Modifier and TypeClassDescriptionstatic @interface
* A wrapper annotation that makes theEnsuresNonNullIf
annotation repeatable. -
Required Element Summary
Modifier and TypeRequired ElementDescriptionString[]
Returns Java expression(s) that are non-null after the method returns the given result.boolean
Returns the return value of the method under which the postcondition holds.
-
Element Details
-
expression
String[] expressionReturns Java expression(s) that are non-null after the method returns the given result.- Returns:
- Java expression(s) that are non-null after the method returns the given result
- See the Checker Framework Manual:
- Syntax of Java expressions
-
result
boolean resultReturns the return value of the method under which the postcondition holds.- Returns:
- the return value of the method under which the postcondition holds
-