1 files changed, 37 insertions, 0 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java
new file mode 100644
index 0000000000..a559c1db27
--- /dev/null
+++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java
@@ -0,0 +1,37 @@
+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 Pure} is a method annotation that means both {@link
+ * SideEffectFree} and {@link Deterministic}.  The more important of these,
+ * when performing pluggable type-checking, is usually {@link
+ * SideEffectFree}.
+ *
+ * @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 Pure {
+    /**
+     * The type of purity.
+     */
+    public static enum Kind {
+        /** The method has no visible side-effects. */
+        SIDE_EFFECT_FREE,
+
+        /**
+         * The method returns exactly the same value when called in the same
+         * environment.
+         */
+        DETERMINISTIC
+    }
+}