1 files changed, 63 insertions, 0 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java
new file mode 100644
index 0000000000..eadcc4f49e
--- /dev/null
+++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java
@@ -0,0 +1,63 @@
+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;
+
+/**
+ * A method is called <em>side-effect-free</em> if it has no visible
+ * side-effects, such as setting a field of an object that existed before
+ * the method was called.
+ * <p>
+ * Only the visible side-effects are important. The method is allowed to cache
+ * the answer to a computationally expensive query, for instance.  It is also
+ * allowed to modify newly-created objects, and a constructor is
+ * side-effect-free if it does not modify any objects that existed before
+ * it was called.
+ * <p>
+ * This annotation is important to pluggable type-checking because if some
+ * fact about an object is known before a call to such a method, then the
+ * fact is still known afterwards, even if the fact is about some non-final
+ * field.  When any non-{@code @SideEffectFree} method is called, then a
+ * pluggable type-checker must assume that any field of any accessible
+ * object might have been modified, which annuls the effect of
+ * flow-sensitive type refinement and prevents the pluggable type-checker
+ * from making conclusions that are obvious to a programmer.
+ * <p>
+ * Also see {@link Pure}, which means both side-effect-free and {@link
+ * Deterministic}.
+ * <p>
+ * <b>Analysis:</b>
+ * The Checker Framework performs a conservative analysis to verify a
+ * {@code @SideEffectFree} annotation.
+ * The Checker Framework issues a warning
+ * if the method uses any of the following Java constructs:
+ * <ol>
+ * <li>Assignment to any expression, except for local variables and method
+ * parameters.
+ * <li>A method invocation of a method that is not {@code @SideEffectFree}.
+ * <li>Construction of a new object where the constructor is not {@code @SideEffectFree}.
+ * </ol>
+ * These rules are conservative:  any code that passes the checks is
+ * side-effect-free, but the Checker Framework may issue false positive
+ * warnings, for code that uses one of the forbidden constructs but is
+ * side-effect-free nonetheless.  In particular, a method that caches its
+ * result will be rejected.
+ * <p>
+ *
+ * In fact, the rules are so conservative that checking is currently
+ * disabled by default, but can be enabled via the
+ * {@code -AcheckPurityAnnotations} command-line option.
+ * <p>
+ *
+ * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and flow-sensitive analysis
+ *
+ * @author Stefan Heule
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ ElementType.METHOD, ElementType.CONSTRUCTOR })
+public @interface SideEffectFree {
+}