EnsuresInitializedFields (checker-framework 3.39.0-eisop1 API)

@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@PostconditionAnnotation(qualifier=InitializedFields.class)
@InheritedAnnotation
@Repeatable(List.class)
public @interface EnsuresInitializedFields

A method postcondition annotation indicates which fields the method definitely initializes.

See the Checker Framework Manual:: Initialized Fields Checker

- Required Element Summary
  
  Required Elements
  Modifier and Type Required Element Description
  
  java.lang.String[] fields
  Fields that this method initializes.
- Optional Element Summary
  
  Optional Elements
  Modifier and Type Optional Element Description
  
  java.lang.String[] value
  The object whose fields this method initializes.

- Element Detail
  - fields
```
@QualifierArgument("value")
java.lang.String[] fields
```
    Fields that this method initializes.
    
    Returns:
    
    fields that this method initializes
- - value
```
java.lang.String[] value
```
    The object whose fields this method initializes.
    
    Returns:
    
    object whose fields are initialized
    
    Default:
    
    {"this"}