Uses of Annotation Type
org.checkerframework.framework.qual.PostconditionAnnotation
Packages that use PostconditionAnnotation
Package
Description
-
Uses of PostconditionAnnotation in org.checkerframework.checker.calledmethods.qual
Classes in org.checkerframework.checker.calledmethods.qual with annotations of type PostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the method, if it terminates successfully, always invokes the given methods on the given expressions. -
Uses of PostconditionAnnotation in org.checkerframework.checker.index.qual
Classes in org.checkerframework.checker.index.qual with annotations of type PostconditionAnnotationModifier and TypeClassDescription@interface
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
A wrapper annotation that makes theEnsuresLTLengthOf
annotation repeatable. -
Uses of PostconditionAnnotation in org.checkerframework.checker.lock.qual
Classes in org.checkerframework.checker.lock.qual with annotations of type PostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the given expressions are held if the method terminates successfully.static @interface
A wrapper annotation that makes theEnsuresLockHeld
annotation repeatable. -
Uses of PostconditionAnnotation in org.checkerframework.checker.nullness.qual
Classes in org.checkerframework.checker.nullness.qual with annotations of type PostconditionAnnotationModifier and TypeClassDescription@interface
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
A wrapper annotation that makes theEnsuresKeyFor
annotation repeatable.@interface
Indicates that the value expressions are non-null just after a method call, if the method terminates successfully.static @interface
A wrapper annotation that makes theEnsuresNonNull
annotation repeatable. -
Uses of PostconditionAnnotation in org.checkerframework.common.initializedfields.qual
Classes in org.checkerframework.common.initializedfields.qual with annotations of type PostconditionAnnotationModifier and TypeClassDescription@interface
A method postcondition annotation indicates which fields the method definitely initializes.static @interface
A wrapper annotation that makes theEnsuresInitializedFields
annotation repeatable.