org.checkerframework.dataflow.qual

Annotation Type TerminatesExecution

@Documented
 @Retention(value=RUNTIME)
 @Target(value={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().

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.

See the Checker Framework Manual:

Automatic type refinement (flow-sensitive type qualifier inference)