Package org.checkerframework.checker.nullness.qual

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 a method establishes a property, even though 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

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
    Returns Java expression(s) that are non-null after the method returns the given result.
    boolean
    result
    Returns the return value of the method under which the postcondition holds.

  • Element Details

    • result

      boolean result
      Returns the return value of the method under which the postcondition holds.
      Returns:
      the return value of the method under which the postcondition holds

    • expression

      String[] expression
      Returns 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