Annotation Interface RequiresPresent
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@PreconditionAnnotation(qualifier=Present.class)
public @interface RequiresPresent
Indicates a method precondition: the specified expressions of type Optional must be present
(i.e., non-empty) when the annotated method is invoked.
For example:
import java.util.Optional;
import org.checkerframework.checker.optional.qual.RequiresPresent;
import org.checkerframework.checker.optional.qual.Present;
class MyClass {
Optional<String> optId1;
Optional<String> optId2;
@RequiresPresent({"optId1", "#1.optId1"})
void method1(MyClass other) {
optId1.get().length() // OK, this.optID1 is known to be present.
optId2.get().length() // error, might throw NoSuchElementException.
other.optId1.get().length() // OK, this.optID1 is known to be present.
other.optId2.get().length() // error, might throw NoSuchElementException.
}
void method2() {
MyClass other = new MyClass();
optId1 = Optional.of("abc");
other.optId1 = Optional.of("def")
method1(other); // OK, satisfies method precondition.
optId1 = Optional.empty();
other.optId1 = Optional.empty("abc");
method1(other); // error, does not satisfy this.optId1 method precondition.
optId1 = Optional.empty("abc");
other.optId1 = Optional.empty();
method1(other); // error. does not satisfy other.optId1 method precondition.
}
}
Do not use this annotation for formal parameters (instead, give them a @Present type).
The @RequiresNonNull annotation is intended for non-parameter expressions, such as field
accesses or method calls.- See the Checker Framework Manual:
- Optional Checker
-
Nested Class Summary
Nested ClassesModifier and TypeClassDescriptionstatic @interfaceA wrapper annotation that makes theRequiresPresentannotation repeatable. -
Required Element Summary
Required Elements
-
Element Details
-
value
String[] valueThe Java expressions that that need to bePresent.- Returns:
- the Java expressions that need to be
Present - See the Checker Framework Manual:
- Syntax of Java expressions
-