Package org.checkerframework.common.initializedfields.qual

Annotation Interface EnsuresInitializedFields

@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

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    fields
    Fields that this method initializes.

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    String[]
    value
    The object whose fields this method initializes.

  • Element Details

    • fields

      @QualifierArgument("value") String[] fields
      Fields that this method initializes.
      Returns:
      fields that this method initializes

    • value

      String[] value
      The object whose fields this method initializes.
      Returns:
      object whose fields are initialized
      Default:
      {"this"}