1 files changed, 38 insertions, 0 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java
new file mode 100644
index 0000000000..cd9d5d8c79
--- /dev/null
+++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java
@@ -0,0 +1,38 @@
+package org.checkerframework.dataflow.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * {@code 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 {@code System.exit()}.
+ * <p>
+
+ * The annotation enables flow-sensitive type refinement to be more
+ * precise.  For example, after
+ * <pre>
+ * if (x == null) {
+ *   System.err.println("Bad value supplied");
+ *   System.exit(1);
+ * }
+ * </pre>
+ * the Nullness Checker can determine that {@code x} is non-null.
+ *
+ * <p>
+ * The annotation is a <em>trusted</em> annotation, meaning that it is not
+ * checked whether the annotated method really does terminate the program.
+ *
+ * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type qualifier inference)
+ *
+ * @author Stefan Heule
+ *
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ ElementType.METHOD, ElementType.CONSTRUCTOR })
+public @interface TerminatesExecution {
+}