Uses of Annotation Interface
org.checkerframework.framework.qual.PostconditionAnnotation

Packages that use PostconditionAnnotation

Package	Description
org.checkerframework.checker.calledmethods.qual
org.checkerframework.checker.index.qual
org.checkerframework.checker.lock.qual
org.checkerframework.checker.nonempty.qual
org.checkerframework.checker.nullness.qual
org.checkerframework.checker.optional.qual
org.checkerframework.common.initializedfields.qual

Uses of PostconditionAnnotation in org.checkerframework.checker.calledmethods.qual

Classes in org.checkerframework.checker.calledmethods.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresCalledMethods	Indicates that the method, if it terminates successfully, always invokes the given methods on the given expressions.
static @interface	EnsuresCalledMethods.List	A wrapper annotation that makes the EnsuresCalledMethods annotation repeatable.

Uses of PostconditionAnnotation in org.checkerframework.checker.index.qual

Classes in org.checkerframework.checker.index.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresLTLengthOf	Indicates that the value expressions evaluate to an integer whose value is less than the lengths of all the given sequences, if the method terminates successfully.
static @interface	EnsuresLTLengthOf.List	A wrapper annotation that makes the EnsuresLTLengthOf annotation repeatable.

Uses of PostconditionAnnotation in org.checkerframework.checker.lock.qual

Classes in org.checkerframework.checker.lock.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresLockHeld	Indicates that the given expressions are held if the method terminates successfully.
static @interface	EnsuresLockHeld.List	A wrapper annotation that makes the EnsuresLockHeld annotation repeatable.

Uses of PostconditionAnnotation in org.checkerframework.checker.nonempty.qual

Classes in org.checkerframework.checker.nonempty.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresNonEmpty	Indicates that a particular expression evaluates to a non-empty value, if the method terminates successfully.

Uses of PostconditionAnnotation in org.checkerframework.checker.nullness.qual

Classes in org.checkerframework.checker.nullness.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresKeyFor	Indicates that the value expressions evaluate to a value that is a key in all the given maps, if the method terminates successfully.
static @interface	EnsuresKeyFor.List	A wrapper annotation that makes the EnsuresKeyFor annotation repeatable.
@interface	EnsuresNonNull	Indicates that the value expressions are non-null just after a method call, if the method terminates successfully.
static @interface	EnsuresNonNull.List	A wrapper annotation that makes the EnsuresNonNull annotation repeatable.

Uses of PostconditionAnnotation in org.checkerframework.checker.optional.qual

Classes in org.checkerframework.checker.optional.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresPresent	Indicates that the expression evaluates to a present Optional, if the method terminates successfully.

Uses of PostconditionAnnotation in org.checkerframework.common.initializedfields.qual

Classes in org.checkerframework.common.initializedfields.qual with annotations of type PostconditionAnnotation

Modifier and Type	Class	Description
@interface	EnsuresInitializedFields	A method postcondition annotation indicates which fields the method definitely initializes.
static @interface	EnsuresInitializedFields.List	A wrapper annotation that makes the EnsuresInitializedFields annotation repeatable.