Uses of Class
org.checkerframework.framework.qual.ConditionalPostconditionAnnotation
-
-
Uses of ConditionalPostconditionAnnotation in org.checkerframework.checker.calledmethods.qual
Classes in org.checkerframework.checker.calledmethods.qual with annotations of type ConditionalPostconditionAnnotation Modifier and Type Class Description interface
EnsuresCalledMethodsIf
Indicates that the method, if it terminates with the given result, invokes the given methods on the given expressions.static interface
EnsuresCalledMethodsIf.List
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 ConditionalPostconditionAnnotation Modifier and Type Class Description interface
EnsuresLTLengthOfIf
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
EnsuresLTLengthOfIf.List
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 ConditionalPostconditionAnnotation Modifier and Type Class Description interface
EnsuresLockHeldIf
Indicates that the given expressions are held if the method terminates successfully and returns the given result (either true or false).static interface
EnsuresLockHeldIf.List
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 ConditionalPostconditionAnnotation Modifier and Type Class Description interface
EnsuresKeyForIf
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
EnsuresKeyForIf.List
A wrapper annotation that makes theEnsuresKeyForIf
annotation repeatable.interface
EnsuresNonNullIf
Indicates that the given expressions are non-null, if the method returns the given result (either true or false).static interface
EnsuresNonNullIf.List
* 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 ConditionalPostconditionAnnotation Modifier and Type Class Description interface
EnsuresMinLenIf
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
EnsuresMinLenIf.List
A wrapper annotation that makes theEnsuresMinLenIf
annotation repeatable.
-