Uses of Class
org.checkerframework.framework.qual.PostconditionAnnotation
-
-
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. -
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 theEnsuresLTLengthOf
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 theEnsuresLockHeld
annotation repeatable. -
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 theEnsuresKeyFor
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 theEnsuresNonNull
annotation repeatable. -
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 theEnsuresInitializedFields
annotation repeatable.
-