Annotation Interface TerminatesExecution
TerminatesExecution is a method annotation that indicates that a method terminates the
execution of the program. This can be used to annotate methods such as System.exit(), or
methods that unconditionally throw an exception.
The annotation enables flow-sensitive type refinement to be more precise. For example, after
if (x == null) {
System.err.println("Bad value supplied");
System.exit(1);
}
the Nullness Checker can determine that x is non-null.
The annotation is a trusted annotation, meaning that it is not checked whether the annotated method really does terminate the program.
This annotation is inherited by subtypes, just as if it were meta-annotated with
@InheritedAnnotation.
The Checker Framework recognizes this annotation, but the Java compiler javac does
not. After calling a method annotated with TerminatesExecution, to prevent a
javac diagnostic, you generally need to insert a throw statement (which you know will
never execute):
...
myTerminatingMethod();
throw new Error("unreachable");
- See the Checker Framework Manual:
- Automatic type refinement (flow-sensitive type
qualifier inference)