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, indicating that the argument is null if the method returns normally:

  /** Throws an exception if the argument is null. */
  @EnsuresNonNull("#1")
  void assertNonNull(Object arg) { ... }
 

See Also:

• EnsuresNonNullIf
• NonNull
• NullnessChecker

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