| 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 <tt>x</tt> 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 { |
| } |