Package org.checkerframework.checker.nullness.qual

Annotation Interface EnsuresNonNull

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @PostconditionAnnotation(qualifier=NonNull.class) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresNonNull
Indicates that the value expressions are non-null just after a method call, if the method terminates successfully.

This postcondition annotation is useful for methods that initialize a field: 


 @EnsuresNonNull("theMap")
  void initialize() {
    theMap = new HashMap<>();
  }
It can also be used for a method that fails if a given expression is null: 

  /** Throws an exception if the argument is null. */
 @EnsuresNonNull("#1")
  void assertNonNull(Object arg) { ... }
See Also:
See the Checker Framework Manual:
Nullness Checker

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    value
    Returns Java expressions that are NonNull after successful method termination.

  • Element Details

    • value

      String[] value
      Returns Java expressions that are NonNull after successful method termination.
      Returns:
      Java expressions that are NonNull after successful method termination
      See the Checker Framework Manual:
      Syntax of Java expressions