Annotation Interface TerminatesExecution

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) public @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");
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):

 throw new Error("unreachable");
See the Checker Framework Manual:
Automatic type refinement (flow-sensitive type qualifier inference)