EnsuresNonNull (checker-framework 3.39.0-eisop1 API)

```
@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

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

- Element Detail
  - value
```
java.lang.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