diff --git a/SKIP-REQUIRE-JAVADOC b/SKIP-REQUIRE-JAVADOC
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/build.gradle b/build.gradle
index 12e19e3b5acf..3a4defcb26fa 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1219,7 +1219,15 @@ subprojects {
       description = "Run the Checker Framework on itself (part 1)"
       group = "Verification"
       dependsOn("checkCompilerMessages", "checkFormatter", "checkInterning", "checkModifiability", "checkOptional")
-      // Can't run "checkPurity" because it issues too many warnings.
+      // The Purity Checker does not yet pass on annotation-file-utilities, checker, dataflow,
+      // or framework.  To work on one of those, run its `checkPurity` task directly, such as
+      // `./gradlew :dataflow:checkPurity`.
+      if (!(project.name.equals("annotation-file-utilities")
+          || project.name.equals("checker")
+          || project.name.equals("dataflow")
+          || project.name.equals("framework"))) {
+        dependsOn("checkPurity")
+      }
     }
     tasks.register("typecheck-part2") {
       description = "Run the Checker Framework on itself (part 2)"
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java b/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java
index 3bf37fea0ab0..3223c888e056 100644
--- a/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java
+++ b/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java
@@ -12,7 +12,7 @@
 import java.util.StringJoiner;
 import org.checkerframework.checker.modifiability.qual.Modifiable;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 /**
@@ -354,7 +354,10 @@ public boolean isAssignableFrom(Class<?> argType) {
   }
 
   /** Returns a pretty-printed {@link ConversionCategory}. */
-  @Pure
+  // This is @SideEffectFree rather than @Pure because it returns a string that differs
+  // according to ==, and @Deterministic requires that two calls return == results.
+  @SideEffectFree
+  @SuppressWarnings("purity") // appends only to a local StringBuilder
   @Override
   public String toString() {
     StringBuilder sb = new StringBuilder(32);
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java b/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
index 165eba213374..607875f3bbcf 100644
--- a/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
+++ b/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
@@ -198,6 +198,7 @@ public boolean isAssignableFrom(Class<?> argType) {
   }
 
   /** Returns a pretty-printed {@link I18nConversionCategory}. */
+  @SuppressWarnings("purity") // appends only to a local StringBuilder
   @Override
   public String toString() {
     StringBuilder sb = new StringBuilder(this.name());
diff --git a/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java b/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java
index 05f17e02b2b5..d2f8560f6714 100644
--- a/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java
+++ b/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java
@@ -294,6 +294,7 @@ public int getFound() {
       return found;
     }
 
+    @SuppressWarnings("purity") // String.format() returns a fresh but always-equal String
     @Override
     public String getMessage() {
       return String.format("Expected %d arguments but found %d.", expected, found);
@@ -325,6 +326,7 @@ public ConversionCategory getFound() {
       return found;
     }
 
+    @SuppressWarnings("purity") // String.format() returns a fresh but always-equal String
     @Override
     public String getMessage() {
       return String.format("Expected category %s but found %s.", expected, found);
diff --git a/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java b/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java
index e697598fcc41..06c3c013775f 100644
--- a/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java
+++ b/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java
@@ -163,7 +163,10 @@ public static boolean isRegex(String s) {
    * @param groups number of groups expected
    * @return true iff s is a regular expression with {@code groups} groups
    */
-  @SuppressWarnings("regex") // RegexUtil
+  @SuppressWarnings({
+    "regex", // RegexUtil
+    "purity" // catch block is a guard; the result depends only on the arguments
+  })
   @Pure
   // @EnsuresQualifierIf annotation is extraneous because this method is special-cased
   // in RegexTransfer.
@@ -185,8 +188,10 @@ public static boolean isRegex(String s, int groups) {
    * @return true iff c is a regular expression
    */
   @SuppressWarnings({
-    "regex", "lock"
-  }) // RegexUtil; temp value used in pure method is equal up to equals but not up to ==
+    "regex", // RegexUtil
+    "lock", // temp value used in pure method is equal up to equals but not up to ==
+    "purity" // Character.toString() returns a fresh but always-equal String
+  })
   @Pure
   @EnsuresQualifierIf(result = true, expression = "#1", qualifier = Regex.class)
   public static boolean isRegex(char c) {
@@ -333,7 +338,10 @@ private static String regexErrorMessage(String s, int expectedGroups, int actual
    * @param p pattern whose groups to count
    * @return the count of groups in the argument
    */
-  @SuppressWarnings("lock") // does not depend on object identity
+  @SuppressWarnings({
+    "lock", // does not depend on object identity
+    "purity" // Pattern.matcher() allocates; the count depends only on the argument
+  })
   @Pure
   private static int getGroupCount(Pattern p) {
     return p.matcher("").groupCount();
diff --git a/checker/tests/lock-records/LockRecord.java b/checker/tests/lock-records/LockRecord.java
index d2bbfcfec397..4102038c2c5d 100644
--- a/checker/tests/lock-records/LockRecord.java
+++ b/checker/tests/lock-records/LockRecord.java
@@ -3,7 +3,6 @@
 
 public record LockRecord(String s, ReentrantLock lock) {
   @LockingFree
-  // :: error: [method.guarantee.violated]
   public LockRecord {
     // :: error: [method.guarantee.violated]
     lock.lock();
diff --git a/checker/tests/nullness/java8/Issue579.java b/checker/tests/nullness/java8/Issue579.java
index 1208899f2b37..66a9fc80df78 100644
--- a/checker/tests/nullness/java8/Issue579.java
+++ b/checker/tests/nullness/java8/Issue579.java
@@ -9,6 +9,7 @@ public class Issue579<T> implements Comparator<T> {
 
   @SideEffectFree
   @SuppressWarnings("unchecked")
+  @SideEffectFree
   Issue579(Comparator<? super T> real) {
     this.real = (Comparator<T>) real;
   }
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java b/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java
index e765cb0626d7..d15d213aa5b7 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java
@@ -8,6 +8,7 @@
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signature.qual.BinaryName;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.plumelib.util.StringsP;
 
 /**
@@ -90,6 +91,7 @@ public List<File> getDiagnosticFiles() {
     return options;
   }
 
+  @SideEffectFree
   @Override
   public List<String> getFlatOptions() {
     return TestUtilities.optionMapToList(options);
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java b/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java
index 49263af5aae1..227afc03f6db 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java
@@ -6,6 +6,7 @@
 import java.util.List;
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 
 /**
  * SimpleOptionMap is a very basic command-line option container. The keys of the option container
@@ -147,6 +148,7 @@ public void addOptions(Iterable<String> newOptions) {
    *
    * @return a list of the string representations of the options in this object
    */
+  @SideEffectFree
   public List<String> getOptionsAsList() {
     return TestUtilities.optionMapToList(options);
   }
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java
index 6f32b83b046f..60072dc711b3 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java
@@ -27,6 +27,7 @@
 import javax.tools.ToolProvider;
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.SystemUtil;
 import org.junit.Assert;
@@ -371,6 +372,8 @@ public static File findComparisonFile(File testFile) {
    * @param options an option map
    * @return return a list of option names
    */
+  @SideEffectFree
+  @SuppressWarnings("purity") // adds only to a newly allocated list
   public static List<String> optionMapToList(Map<String, @Nullable String> options) {
     List<String> optionList = new ArrayList<>(options.size() * 2);
 
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java
index 422e7e8794f1..566c9dec8ffa 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java
@@ -3,6 +3,7 @@
 import java.util.LinkedHashMap;
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.Pure;
 
 /** The kinds of errors that can be encountered during typechecking. */
 public enum DiagnosticKind {
@@ -31,6 +32,7 @@ public enum DiagnosticKind {
   }
 
   /** Convert a string as it would appear in error messages or source code into a DiagnosticKind. */
+  @Pure
   public static @Nullable DiagnosticKind fromParseString(String parseStr) {
     return stringToCategory.get(parseStr);
   }
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java
index a2203acd4f97..a3b867c244a6 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java
@@ -18,6 +18,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.RequiresNonNull;
 import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.dataflow.qual.SideEffectsOnly;
 
 /**
@@ -145,6 +146,7 @@ private interface StringToTestDiagnosticLine {
      * @param lineNumber the line number of the line
      * @return TestDiagnosticLine corresponding to {@code line}
      */
+    @SideEffectFree
     TestDiagnosticLine createTestDiagnosticLine(String filename, String line, long lineNumber);
   }
 
@@ -268,6 +270,7 @@ public TestDiagnosticLine next() {
    * @throws IOException if there is trouble while reading
    */
   @RequiresNonNull("reader")
+  @SideEffectsOnly("this")
   /*package-private*/ void advance(@UnknownInitialization JavaDiagnosticReader this)
       throws IOException {
     nextLine = reader.readLine();
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java
index 7d186475eae9..5bff9aa409e7 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java
@@ -2,6 +2,8 @@
 
 import java.util.Objects;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 
 /**
  * Represents an expected error/warning message in a Java test file or an error/warning reported by
@@ -44,6 +46,7 @@ public class TestDiagnostic {
    * @param isFixable true if this diagnostic should no longer be reported after whole-program
    *     inference
    */
+  @SideEffectFree
   public TestDiagnostic(
       String filename,
       long lineNumber,
@@ -63,6 +66,7 @@ public String getFilename() {
     return filename;
   }
 
+  @Pure
   public long getLineNumber() {
     return lineNumber;
   }
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java
index 7c12461db61d..37a5a63ace31 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java
@@ -1,6 +1,7 @@
 package org.checkerframework.framework.test.diagnostics;
 
 import java.util.List;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 
 /** Represents a list of TestDiagnostics, which was read from a one line of a file. */
 public class TestDiagnosticLine {
@@ -9,6 +10,7 @@ public class TestDiagnosticLine {
   private final String originalLine;
   private final List<TestDiagnostic> diagnostics;
 
+  @SideEffectFree
   public TestDiagnosticLine(
       String filename, long lineNumber, String originalLine, List<TestDiagnostic> diagnostics) {
     this.filename = filename;
diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java
index 011fecb84c5f..ef4012663905 100644
--- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java
+++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java
@@ -12,6 +12,7 @@
 import javax.tools.JavaFileObject;
 import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.javacutil.BugInCF;
 import org.plumelib.util.CollectionsP;
 
@@ -97,6 +98,7 @@ private TestDiagnosticUtils() {
    * @param stringFromDiagnosticFile a single diagnostic string to parse
    * @return a new TestDiagnostic
    */
+  @SideEffectFree
   public static TestDiagnostic fromDiagnosticFileString(String stringFromDiagnosticFile) {
     return fromPatternMatching(
         DIAGNOSTIC_FILE_PATTERN,
@@ -116,6 +118,7 @@ public static TestDiagnostic fromDiagnosticFileString(String stringFromDiagnosti
    * @param stringFromJavaFile the string containing the diagnostic
    * @return a new TestDiagnostic
    */
+  @SideEffectFree
   public static TestDiagnostic fromJavaFileComment(
       String filename, long lineNumber, String stringFromJavaFile) {
     return fromPatternMatching(
@@ -155,6 +158,7 @@ public static TestDiagnostic fromJavaxToolsDiagnostic(String diagnosticString) {
    * @param stringFromJavaFile the string containing the diagnostic
    * @return a new TestDiagnostic
    */
+  @SideEffectFree
   public static TestDiagnostic fromJSpecifyFileComment(
       String filename, long lineNumber, String stringFromJavaFile) {
     return new TestDiagnostic(
@@ -177,6 +181,7 @@ public static TestDiagnostic fromJSpecifyFileComment(
    * @param diagnosticString the string to parse
    * @return a diagnostic parsed from the given string
    */
+  @SideEffectFree
   @SuppressWarnings({
     "nullness", // TODO: regular expression group access
     "regex:group.count" // group count varies by pattern; callers ensure correct group counts
@@ -350,6 +355,7 @@ private static boolean retainAllLines(String message) {
    * @param category a category string that may be prepended with "fixable-"
    * @return the category and whether it was prepended with "fixable-"
    */
+  @SideEffectFree
   private static CategoryAndFixable categoryAndFixable(String category) {
     String fixable = "fixable-";
     boolean isFixable = category.startsWith(fixable);
@@ -370,12 +376,17 @@ private static CategoryAndFixable categoryAndFixable(String category) {
    * @param kind the diagnostic category
    * @param isFixable true if the category string was prepended with "fixable-"
    */
-  private record CategoryAndFixable(DiagnosticKind kind, boolean isFixable) {}
+  private record CategoryAndFixable(DiagnosticKind kind, boolean isFixable) {
+    /** Creates a CategoryAndFixable. */
+    @SideEffectFree
+    CategoryAndFixable {}
+  }
 
   /**
    * Returns true if this line in a Java file indicates an expected diagnostic that might be
    * continued on the next line.
    */
+  @SideEffectFree
   public static boolean isJavaDiagnosticLineStart(String originalLine) {
     String trimmedLine = originalLine.trim();
     return trimmedLine.startsWith("// ::") || trimmedLine.startsWith("// warning:");
@@ -395,6 +406,7 @@ public static boolean isJavaDiagnosticLineStart(String originalLine) {
    * (to avoid false positive matches, such as when "// ::" is commented out in source code). It
    * could be extended in the future if such an extension is necessary.
    */
+  @SideEffectFree
   public static String handleEndOfLineJavaDiagnostic(String originalLine) {
     int curlyIndex = originalLine.indexOf("{ // ::");
     if (curlyIndex == -1) {
@@ -406,6 +418,7 @@ public static String handleEndOfLineJavaDiagnostic(String originalLine) {
 
   /** Return true if this line in a Java file continues an expected diagnostic. */
   @EnsuresNonNullIf(result = true, expression = "#1")
+  @SideEffectFree
   public static boolean isJavaDiagnosticLineContinuation(@Nullable String originalLine) {
     if (originalLine == null) {
       return false;
@@ -421,6 +434,7 @@ public static boolean isJavaDiagnosticLineContinuation(@Nullable String original
    * Returns the continuation part. The argument is such that {@link
    * #isJavaDiagnosticLineContinuation} returns true.
    */
+  @SideEffectFree
   public static String continuationPart(String originalLine) {
     return originalLine.trim().substring(2).trim();
   }
@@ -431,6 +445,8 @@ public static String continuationPart(String originalLine) {
    * <p>The input {@code line} is possibly the concatenation of multiple source lines, if the
    * diagnostic was split across lines in the source code.
    */
+  @SideEffectFree
+  @SuppressWarnings("purity") // CollectionsP.mapList is side-effect-free but unannotated
   public static TestDiagnosticLine fromJavaSourceLine(
       String filename, String line, long lineNumber) {
     String trimmedLine = line.trim();
@@ -475,6 +491,7 @@ public static TestDiagnosticLine fromJavaSourceLine(
   }
 
   /** Convert a line in a DiagnosticFile to a TestDiagnosticLine. */
+  @SideEffectFree
   public static TestDiagnosticLine fromDiagnosticFileLine(String diagnosticLine) {
     String trimmedLine = diagnosticLine.trim();
     if (trimmedLine.startsWith("#") || trimmedLine.isEmpty()) {
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java b/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java
index 36f33920dceb..83777f656d10 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java
@@ -153,7 +153,12 @@ public void typeProcessingOver() {
    *
    * @return the compiler log, which contains errors and warnings
    */
+  // Log.instance() constructs the Log and registers it in the compiler Context on its first
+  // call, so it is not strictly side-effect-free.  @SideEffectFree is retained because javac
+  // creates the Log before any annotation processor runs, and because callers rely on it to
+  // preserve field refinements across the call.
   @SideEffectFree
+  @SuppressWarnings("purity") // Log.instance() registers the Log in the Context on the first call
   public Log getCompilerLog() {
     return Log.instance(((JavacProcessingEnvironment) processingEnv).getContext());
   }
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java
index 1e6115e528d7..75c840d0bccc 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java
@@ -32,6 +32,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signature.qual.CanonicalName;
 import org.checkerframework.checker.signature.qual.FullyQualifiedName;
+import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.plumelib.reflection.ReflectionP;
 import org.plumelib.util.ArrayMap;
@@ -832,6 +833,7 @@ public DeclaredType getAnnotationType() {
     }
 
     @SideEffectFree
+    @SuppressWarnings("purity") // mutates only local builders and memoizes toString
     @Override
     public String toString() {
       if (toStringVal != null) {
@@ -875,12 +877,14 @@ private static class CheckerFrameworkAnnotationValue implements AnnotationValue
       this.value = obj;
     }
 
+    @Pure
     @Override
     public Object getValue() {
       return value;
     }
 
     @SideEffectFree
+    @SuppressWarnings("purity") // mutates only a local String and memoizes toString
     @Override
     public String toString() {
       if (this.toStringVal != null) {
@@ -944,6 +948,7 @@ public <R, P> R accept(AnnotationValueVisitor<R, P> v, P p) {
       }
     }
 
+    @SuppressWarnings("purity") // getValue() may allocate; comparison is by content
     @Override
     public boolean equals(@Nullable Object obj) {
       // System.out.printf("Calling CFAV.equals()%n");
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java
index b88da0781242..bea1905f0aeb 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java
@@ -27,6 +27,12 @@
  * <p>AnnotationMirror is an interface and not all implementing classes provide a correct equals
  * method; therefore, existing implementations of Map cannot be used.
  */
+// Every @Pure method inherited from Map (containsKey, get, equals, hashCode) iterates a
+// collection, which the Purity Checker cannot verify: Collection.iterator() and
+// Map.keySet()/entrySet() are @SideEffectFree but not @Deterministic, because each call
+// allocates a fresh iterator or view, and Iterator.next() mutates it.  The catch block in
+// equals() is likewise forbidden in a @Deterministic method.
+@SuppressWarnings("purity")
 public class AnnotationMirrorMap<V> implements Map<@KeyFor("this") AnnotationMirror, V> {
 
   /** The actual map to which all work is delegated. */
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java
index 51719fb685ac..f22d1fe49df5 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java
@@ -14,6 +14,7 @@
 import org.checkerframework.checker.nullness.qual.PolyNull;
 import org.checkerframework.common.returnsreceiver.qual.This;
 import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.dataflow.qual.SideEffectsOnly;
 import org.plumelib.util.DeepCopyable;
 
@@ -46,6 +47,7 @@ public class AnnotationMirrorSet
   // Constructors and factory methods
 
   /** Default constructor. */
+  @SideEffectFree
   public AnnotationMirrorSet() {}
 
   // TODO: Should this be an unmodifiable set?
@@ -135,6 +137,7 @@ public boolean isEmpty() {
     return shadowSet.isEmpty();
   }
 
+  @SuppressWarnings("purity") // containsSame iterates the set
   @Override
   public boolean contains(
       @UnknownInitialization(AnnotationMirrorSet.class) AnnotationMirrorSet this,
@@ -261,6 +264,7 @@ public boolean equals(@Nullable Object o) {
     return containsAll(s);
   }
 
+  @SuppressWarnings("purity") // iterates the set
   @Override
   public int hashCode() {
     int result = 0;
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java
index 2c4da7029e79..53ff684d091b 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java
@@ -71,7 +71,8 @@ private AnnotationUtils() {
    * @param annotation the annotation whose name to return
    * @return the fully-qualified name of an annotation as a String
    */
-  public static final @CanonicalName String annotationName(AnnotationMirror annotation) {
+  @SideEffectFree
+  public static @CanonicalName String annotationName(AnnotationMirror annotation) {
     if (annotation instanceof AnnotationBuilder.CheckerFrameworkAnnotationMirror cfam) {
       return cfam.annotationName;
     }
@@ -127,6 +128,7 @@ private AnnotationUtils() {
    * @return true iff a1 and a2 are the same annotation
    */
   @EqualsMethod
+  @SideEffectFree
   public static boolean areSame(AnnotationMirror a1, AnnotationMirror a2) {
     if (a1 == a2) {
       return true;
@@ -150,6 +152,7 @@ public static boolean areSame(AnnotationMirror a1, AnnotationMirror a2) {
    * @see #areSame(AnnotationMirror, AnnotationMirror)
    */
   @EqualsMethod
+  @SideEffectFree
   public static int compareByName(AnnotationMirror a1, AnnotationMirror a2) {
     if (a1 == a2) {
       return 0;
@@ -186,6 +189,7 @@ public static int compareByName(AnnotationMirror a1, AnnotationMirror a2) {
    * @see #areSame(AnnotationMirror, AnnotationMirror)
    */
   @EqualsMethod
+  @SideEffectFree
   public static boolean areSameByName(AnnotationMirror a1, AnnotationMirror a2) {
     if (a1 == a2) {
       return true;
@@ -285,6 +289,7 @@ public static boolean containsSame(
    * @return AnnotationMirror with the same class as {@code anno} iff c contains anno, according to
    *     areSame; otherwise, {@code null}
    */
+  @SideEffectFree
   public static @Nullable AnnotationMirror getSame(
       Collection<? extends AnnotationMirror> c, AnnotationMirror anno) {
     for (AnnotationMirror an : c) {
@@ -403,6 +408,7 @@ public static boolean containsSameByName(
    * @return an ordering over AnnotationMirrors based on their name and values
    */
   @Pure
+  @SuppressWarnings("purity") // mutates only a newly allocated set
   public static int compareAnnotationMirrors(AnnotationMirror a1, AnnotationMirror a2) {
     int nameComparison = compareByName(a1, a2);
     if (nameComparison != 0) {
@@ -443,6 +449,7 @@ public static int compareAnnotationMirrors(AnnotationMirror a1, AnnotationMirror
    * @return -1 if the first is lesser, 0 if they are the same, or 1 if the first is greater
    */
   @CompareToMethod
+  @SideEffectFree
   private static int compareAnnotationValue(AnnotationValue av1, AnnotationValue av2) {
     if (av1 == av2) {
       return 0;
@@ -463,6 +470,7 @@ private static int compareAnnotationValue(AnnotationValue av1, AnnotationValue a
    *     than, equal to, or greater than the second annotation value
    */
   @CompareToMethod
+  @SideEffectFree
   private static int compareAnnotationValueValue(@Nullable Object val1, @Nullable Object val2) {
     if (val1 == val2) {
       return 0;
@@ -711,7 +719,7 @@ private static class NoSuchElementException extends BugInCF {
      *
      * @param message the detail message
      */
-    @Pure
+    @SideEffectFree
     public NoSuchElementException(String message) {
       super(message);
     }
@@ -1188,6 +1196,7 @@ public static <T extends Enum<T>> T[] annotationValueListToEnumArray(
    * @return true if the two annotations have the same elements (fields)
    */
   @EqualsMethod
+  @SideEffectFree
   private static boolean sameElementValues(AnnotationMirror am1, AnnotationMirror am2) {
 
     // This method might return true even if these maps differ, because of default values.
@@ -1258,6 +1267,7 @@ private static boolean sameElementValues(AnnotationMirror am1, AnnotationMirror
    * @param av2 the second AnnotationValue to compare
    * @return true if the two annotation values are the same
    */
+  @SideEffectFree
   public static boolean sameAnnotationValue(AnnotationValue av1, AnnotationValue av2) {
     return compareAnnotationValue(av1, av2) == 0;
   }
@@ -1503,6 +1513,7 @@ public static boolean hasTypeQualifierElementTypes(ElementType[] elements, Class
    * @return the string representation, using simple (not fully-qualified) names
    */
   @SideEffectFree
+  @SuppressWarnings("purity") // mutates only a newly allocated StringJoiner
   public static String toStringSimple(AnnotationMirrorSet annos) {
     DefaultAnnotationFormatter defaultAnnotationFormatter = new DefaultAnnotationFormatter();
     StringJoiner result = new StringJoiner(" ");
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java b/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java
index a7fd353e2ec4..75591ca644c8 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java
@@ -3,6 +3,8 @@
 import com.sun.source.tree.Tree;
 import org.checkerframework.checker.formatter.qual.FormatMethod;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 
 /**
  * Exception type indicating a bug in the framework.
@@ -22,6 +24,7 @@ public class BugInCF extends RuntimeException {
    *
    * @param message the detail message
    */
+  @SideEffectFree
   public BugInCF(String message) {
     this(message, new Throwable());
   }
@@ -34,6 +37,7 @@ public BugInCF(String message) {
    * @param args the arguments for the format string
    */
   @FormatMethod
+  @SideEffectFree
   public BugInCF(String fmt, @Nullable Object... args) {
     this(String.format(fmt, args), new Throwable());
   }
@@ -43,6 +47,7 @@ public BugInCF(String fmt, @Nullable Object... args) {
    *
    * @param cause the cause; its detail message will be used and must be non-null
    */
+  @SideEffectFree
   public BugInCF(Throwable cause) {
     this((Tree) null, cause);
   }
@@ -53,6 +58,7 @@ public BugInCF(Throwable cause) {
    * @param location where to report the bug
    * @param cause the cause; its detail message will be used and must be non-null
    */
+  @SideEffectFree
   public BugInCF(@Nullable Tree location, Throwable cause) {
     this(
         location,
@@ -69,6 +75,7 @@ public BugInCF(@Nullable Tree location, Throwable cause) {
    * @param args the arguments for the format string
    */
   @FormatMethod
+  @SideEffectFree
   public BugInCF(Throwable cause, String fmt, @Nullable Object... args) {
     this(String.format(fmt, args), cause);
   }
@@ -79,6 +86,7 @@ public BugInCF(Throwable cause, String fmt, @Nullable Object... args) {
    * @param message the detail message
    * @param cause the cause
    */
+  @SideEffectFree
   public BugInCF(String message, Throwable cause) {
     this(null, message, cause);
   }
@@ -90,6 +98,7 @@ public BugInCF(String message, Throwable cause) {
    * @param message the detail message
    * @param cause the cause
    */
+  @SideEffectFree
   public BugInCF(@Nullable Tree location, String message, Throwable cause) {
     super(message, cause);
     if (cause instanceof BugInCF bugInCf && bugInCf.getLocation() != null) {
@@ -110,6 +119,7 @@ public BugInCF(@Nullable Tree location, String message, Throwable cause) {
    *
    * @return the tree at which to report the exception
    */
+  @Pure
   public @Nullable Tree getLocation() {
     return location;
   }
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java b/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java
index 3c479ed5b62b..c163802a5f76 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java
@@ -16,6 +16,7 @@
 /** A utility for converting AnnotationMirrors to Strings. It omits full package names. */
 public class DefaultAnnotationFormatter implements AnnotationFormatter {
   /** Creates a DefaultAnnotationFormatter. */
+  @SideEffectFree
   public DefaultAnnotationFormatter() {}
 
   /**
@@ -46,6 +47,7 @@ public static boolean isInvisibleQualified(AnnotationMirror anno) {
    */
   @Override
   @SideEffectFree
+  @SuppressWarnings("purity") // appends only to a local StringBuilder
   public String formatAnnotationString(
       Collection<? extends AnnotationMirror> annos, boolean printInvisible) {
     StringBuilder sb = new StringBuilder();
@@ -73,6 +75,7 @@ public String formatAnnotationString(
    */
   @Override
   @SideEffectFree
+  @SuppressWarnings("purity") // appends only to a local StringBuilder
   public String formatAnnotationMirror(AnnotationMirror anno) {
     StringBuilder sb = new StringBuilder();
     formatAnnotationMirror(anno, sb);
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
index 9376d4c5604a..7884cf383813 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
@@ -276,6 +276,7 @@ public static boolean isSelfAccess(ExpressionTree tree) {
    * @param tree an expression tree
    * @return the outermost non-parenthesized tree enclosed by the given tree
    */
+  @Pure
   @SuppressWarnings("interning:return") // polymorphism implementation
   public static @PolyInterned ExpressionTree withoutParens(@PolyInterned ExpressionTree tree) {
     ExpressionTree t = tree;
@@ -292,6 +293,7 @@ public static boolean isSelfAccess(ExpressionTree tree) {
    * @param tree an expression tree
    * @return the outermost non-parenthesized non-cast tree enclosed by the given tree
    */
+  @Pure
   @SuppressWarnings("interning:return") // polymorphism implementation
   public static @PolyInterned ExpressionTree withoutParensOrCasts(
       @PolyInterned ExpressionTree tree) {
@@ -322,6 +324,7 @@ public static boolean isSelfAccess(ExpressionTree tree) {
    * @param tree class declaration
    * @return the element for the given class, or null if {@code tree} has not been attributed
    */
+  @Pure
   public static @Nullable TypeElement elementFromDeclaration(ClassTree tree) {
     TypeElement result = (TypeElement) TreeInfo.symbolFor((JCTree) tree);
     return result;
@@ -541,6 +544,7 @@ public static ExecutableElement elementFromUse(MemberReferenceTree tree) {
    * @param tree a method declaration
    * @return the element for the given method
    */
+  @Pure
   public static @Nullable ExecutableElement elementFromDeclaration(MethodTree tree) {
     ExecutableElement result = (ExecutableElement) TreeInfo.symbolFor((JCTree) tree);
     return result;
@@ -629,6 +633,7 @@ public static ExecutableElement elementFromUse(NewClassTree tree) {
    * @param tree the variable
    * @return the element for the given variable, or null if {@code tree} has not been attributed
    */
+  @Pure
   public static @Nullable VariableElement elementFromDeclaration(VariableTree tree) {
     VariableElement result = (VariableElement) TreeInfo.symbolFor((JCTree) tree);
     // `result` is null for a local variable whose enclosing top-level class has not yet been
@@ -1115,6 +1120,7 @@ public static Set<Tree.Kind> classAndMethodTreeKinds() {
    *
    * @return the set of kinds that represent classes
    */
+  @Pure
   public static Set<Tree.Kind> classTreeKinds() {
     return classTreeKinds;
   }
@@ -1125,6 +1131,7 @@ public static Set<Tree.Kind> classTreeKinds() {
    * @param tree the tree to test
    * @return true, iff the given kind is a class kind
    */
+  @Pure
   public static boolean isClassTree(Tree tree) {
     return classTreeKinds().contains(tree.getKind());
   }
@@ -1654,6 +1661,7 @@ public static VariableElement getField(
    * @param tree the Tree to test
    * @return true if the tree is an ExpressionTree
    */
+  @Pure
   public static boolean isExpressionTree(Tree tree) {
     return tree instanceof ExpressionTree;
   }
@@ -1680,6 +1688,7 @@ public static boolean isEnumSuperCall(MethodInvocationTree tree) {
    * @param tree the Tree to test
    * @return true if the tree is a type declaration
    */
+  @Pure
   public static boolean isTypeDeclaration(Tree tree) {
     return isClassTree(tree) || tree instanceof TypeParameterTree;
   }
@@ -1859,6 +1868,7 @@ public static boolean isLocalVariable(Tree tree) {
    *
    * @return the type as a TypeMirror of {@code tree}
    */
+  @Pure
   public static TypeMirror typeOf(Tree tree) {
     return ((JCTree) tree).type;
   }
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java
index ddf855c42600..df4dd0db1ba4 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java
@@ -18,7 +18,7 @@
  * This class contains utility methods for reflectively accessing Tree classes and methods that were
  * added after Java 11.
  */
-@SuppressWarnings("PMD.MissingStaticMethodInNonInstantiatableClass")
+@SuppressWarnings({"PMD.MissingStaticMethodInNonInstantiatableClass", "purity"})
 @Deprecated(forRemoval = true, since = "4.0.0")
 public final class TreeUtilsAfterJava11 {
 
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java
index 403c9aab08a5..a1bacfde7f11 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java
@@ -48,6 +48,7 @@
 import org.checkerframework.checker.signature.qual.CanonicalNameOrEmpty;
 import org.checkerframework.checker.signature.qual.DotSeparatedIdentifiers;
 import org.checkerframework.checker.signature.qual.FullyQualifiedName;
+import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.plumelib.util.CollectionsP;
 import org.plumelib.util.ImmutableTypes;
 import org.plumelib.util.StringsP;
@@ -296,6 +297,7 @@ public static TypeMirror getInnermostComponentType(ArrayType arrayType) {
    * @param t2 the second type to test
    * @return true if the arguments are the same declared types
    */
+  @SideEffectFree
   public static boolean areSameDeclaredTypes(Type.ClassType t1, Type.ClassType t2) {
     // Do a cheaper test first
     if (t1.tsym.name != t2.tsym.name) {