1 files changed, 0 insertions, 54 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
deleted file mode 100644
index 6a969c4364..0000000000
--- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java
+++ /dev/null
@@ -1,54 +0,0 @@
-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 {}