Uses of Annotation Type
org.checkerframework.framework.qual.ConditionalPostconditionAnnotation
Packages that use ConditionalPostconditionAnnotation
Package
Description
-
Uses of ConditionalPostconditionAnnotation in org.checkerframework.checker.calledmethods.qual
Classes in org.checkerframework.checker.calledmethods.qual with annotations of type ConditionalPostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the method, if it terminates with the given result, invokes the given methods on the given expressions.static @interface
A wrapper annotation that makes theEnsuresCalledMethodsIf
annotation repeatable. -
Uses of ConditionalPostconditionAnnotation in org.checkerframework.checker.index.qual
Classes in org.checkerframework.checker.index.qual with annotations of type ConditionalPostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the given expressions evaluate to an integer whose value is less than the lengths of all the given sequences, if the method returns the given result (either true or false).static @interface
A wrapper annotation that makes theEnsuresLTLengthOfIf
annotation repeatable. -
Uses of ConditionalPostconditionAnnotation in org.checkerframework.checker.lock.qual
Classes in org.checkerframework.checker.lock.qual with annotations of type ConditionalPostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the given expressions are held if the method terminates successfully and returns the given result (either true or false).static @interface
A wrapper annotation that makes theEnsuresLockHeldIf
annotation repeatable. -
Uses of ConditionalPostconditionAnnotation in org.checkerframework.checker.nullness.qual
Classes in org.checkerframework.checker.nullness.qual with annotations of type ConditionalPostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the given expressions evaluate to a value that is a key in all the given maps, if the method returns the given result (either true or false).static @interface
A wrapper annotation that makes theEnsuresKeyForIf
annotation repeatable.@interface
Indicates that the given expressions are non-null, if the method returns the given result (either true or false).static @interface
* A wrapper annotation that makes theEnsuresNonNullIf
annotation repeatable. -
Uses of ConditionalPostconditionAnnotation in org.checkerframework.common.value.qual
Classes in org.checkerframework.common.value.qual with annotations of type ConditionalPostconditionAnnotationModifier and TypeClassDescription@interface
Indicates that the value of the given expression is a sequence containing at least the given number of elements, if the method returns the given result (either true or false).static @interface
A wrapper annotation that makes theEnsuresMinLenIf
annotation repeatable.