org.checkerframework.checker.nullness.qual

Annotation Type EnsuresNonNullIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=NonNull.class)
 @InheritedAnnotation
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 cannot write two @EnsuresNonNullIf annotations on a single method; to get the effect of

     @EnsuresNonNullIf(expression="outputFile", result=true)
     @EnsuresNonNullIf(expression="memoryOutputStream", result=false)
     public boolean isThresholdExceeded() { ... }
 

you need to instead write

  @EnsuresQualifiersIf({
    @EnsuresQualifierIf(result=true, qualifier=NonNull.class, expression="outputFile"),
    @EnsuresQualifierIf(result=false, qualifier=NonNull.class, expression="memoryOutputStream")
 })
 

See Also:

NonNull, EnsuresNonNull, NullnessChecker

See the Checker Framework Manual:

Nullness Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	expression Java expression(s) that are non-null after the method returns the given result.
boolean	result The return value of the method that needs to hold for the postcondition to hold.

Element Detail

expression

public abstract String[] expression

Java expression(s) that are non-null after the method returns the given result.

See the Checker Framework Manual:

Syntax of Java expressions

result

public abstract boolean result

The return value of the method that needs to hold for the postcondition to hold.