org.checkerframework.common.initializedfields.qual

Annotation Type EnsuresInitializedFields

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @PostconditionAnnotation(qualifier=InitializedFields.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresInitializedFields.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 and Description
String[]	fields Fields that this method initializes.

Optional Element Summary

Optional Elements

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

Element Detail

fields

@QualifierArgument(value="value")
public abstract String[] fields

Fields that this method initializes.

Returns:

fields that this method initializes

value

public abstract String[] value

The object whose fields this method initializes.

Returns:

object whose fields are initialized

Default:

"this"