diff --git a/checker-qual.jar b/checker-qual.jar
index 6fd66597188d..1f4c88a8511f 100644
Binary files a/checker-qual.jar and b/checker-qual.jar differ
diff --git a/src/java.base/share/classes/org/checkerframework/checker/builder/qual/CalledMethods.java b/src/java.base/share/classes/org/checkerframework/checker/builder/qual/CalledMethods.java
index 8ae314c7fcdb..bc457c6a7979 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/builder/qual/CalledMethods.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/builder/qual/CalledMethods.java
@@ -21,7 +21,7 @@
   /**
    * The names of methods that have definitely been called.
    *
-   * @return the names of methods that have definetely been called
+   * @return the names of methods that have definitely been called
    */
   String[] value();
 }
diff --git a/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/ConversionCategory.java b/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/ConversionCategory.java
index 07c28dc621ce..9d76da93e24e 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/ConversionCategory.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/ConversionCategory.java
@@ -96,7 +96,7 @@ public enum ConversionCategory {
 
   /**
    * Use if no object of any type can be passed as parameter. In this case, the only legal value is
-   * null. This is seldomly needed, and indicates an error in most cases. For example:
+   * null. This is seldom needed, and indicates an error in most cases. For example:
    *
    * <pre>
    *   format("Test %1$f %1$d", null);
@@ -107,8 +107,8 @@ public enum ConversionCategory {
   NULL(null),
 
   /**
-   * Use if a parameter is not used by the formatter. This is seldomly needed, and indicates an
-   * error in most cases. For example:
+   * Use if a parameter is not used by the formatter. This is seldom needed, and indicates an error
+   * in most cases. For example:
    *
    * <pre>
    *   format("Test %1$s %3$s", "a","unused","b");
@@ -187,8 +187,9 @@ public enum ConversionCategory {
    * The conversion categories that have a corresponding conversion character. This lacks UNUSED,
    * TIME_AND_INT, etc.
    */
-  private static final ConversionCategory[] conversionCategoriesWithChar =
-      new ConversionCategory[] {GENERAL, CHAR, INT, FLOAT, TIME};
+  private static final ConversionCategory[] conversionCategoriesWithChar = {
+    GENERAL, CHAR, INT, FLOAT, TIME
+  };
 
   /**
    * Converts a conversion character to a category. For example:
@@ -210,6 +211,13 @@ public static ConversionCategory fromConversionChar(char c) {
     throw new IllegalArgumentException("Bad conversion character " + c);
   }
 
+  /**
+   * Converts an array to a set.
+   *
+   * @param a an array
+   * @param <E> the type of array and set elements
+   * @return a set containing the array's elements
+   */
   private static <E> Set<E> arrayToSet(E[] a) {
     return new HashSet<>(Arrays.asList(a));
   }
@@ -219,11 +227,12 @@ public static boolean isSubsetOf(ConversionCategory a, ConversionCategory b) {
   }
 
   /** Conversion categories that need to be considered by {@link #intersect}. */
-  private static final ConversionCategory[] conversionCategoriesForIntersect =
-      new ConversionCategory[] {CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL};
+  private static final ConversionCategory[] conversionCategoriesForIntersect = {
+    CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL
+  };
 
   /**
-   * Returns the intersection of two categories. This is seldomly needed.
+   * Returns the intersection of two categories. This is seldom needed.
    *
    * <blockquote>
    *
@@ -266,15 +275,16 @@ public static ConversionCategory intersect(ConversionCategory a, ConversionCateg
         return v;
       }
     }
-    throw new RuntimeException();
+    throw new RuntimeException("Could not compute intersect(" + a + ", " + b + ")");
   }
 
   /** Conversion categories that need to be considered by {@link #union}. */
-  private static final ConversionCategory[] conversionCategoriesForUnion =
-      new ConversionCategory[] {NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME};
+  private static final ConversionCategory[] conversionCategoriesForUnion = {
+    NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME
+  };
 
   /**
-   * Returns the union of two categories. This is seldomly needed.
+   * Returns the union of two categories. This is seldom needed.
    *
    * <blockquote>
    *
@@ -346,7 +356,7 @@ public boolean isAssignableFrom(Class<?> argType) {
   @Pure
   @Override
   public String toString() {
-    StringBuilder sb = new StringBuilder();
+    StringBuilder sb = new StringBuilder(32);
     sb.append(name());
     sb.append(" conversion category");
 
@@ -358,7 +368,7 @@ public String toString() {
     for (Class<?> cls : types) {
       sj.add(cls.getSimpleName());
     }
-    sb.append(" ");
+    sb.append(' ');
     sb.append(sj);
 
     return sb.toString();
diff --git a/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/FormatBottom.java b/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/FormatBottom.java
index 9ce0ec040f52..87263ecb9b04 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/FormatBottom.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/formatter/qual/FormatBottom.java
@@ -21,5 +21,5 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @SubtypeOf({Format.class, InvalidFormat.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface FormatBottom {}
diff --git a/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java b/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
index 0438bbfdf3cc..3d99894418eb 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
@@ -64,8 +64,7 @@ public enum I18nConversionCategory {
   }
 
   /** Used by {@link #stringToI18nConversionCategory}. */
-  private static final I18nConversionCategory[] namedCategories =
-      new I18nConversionCategory[] {DATE, NUMBER};
+  private static final I18nConversionCategory[] namedCategories = {DATE, NUMBER};
 
   /**
    * Creates a conversion cagetogry from a string name.
@@ -90,6 +89,13 @@ public static I18nConversionCategory stringToI18nConversionCategory(String strin
     throw new IllegalArgumentException("Invalid format type " + string);
   }
 
+  /**
+   * Converts an array to a set.
+   *
+   * @param a an array
+   * @param <E> the type of array and set elements
+   * @return a set containing the array's elements
+   */
   private static <E> Set<E> arrayToSet(E[] a) {
     return new HashSet<>(Arrays.asList(a));
   }
@@ -104,8 +110,7 @@ public static boolean isSubsetOf(I18nConversionCategory a, I18nConversionCategor
   }
 
   /** Conversion categories that need to be considered by {@link #intersect}. */
-  private static final I18nConversionCategory[] conversionCategoriesForIntersect =
-      new I18nConversionCategory[] {DATE, NUMBER};
+  private static final I18nConversionCategory[] conversionCategoriesForIntersect = {DATE, NUMBER};
 
   /**
    * Returns the intersection of the two given I18nConversionCategories.
@@ -147,7 +152,7 @@ public static I18nConversionCategory intersect(
         return v;
       }
     }
-    throw new RuntimeException();
+    throw new RuntimeException("Could not compute intersect(" + a + ", " + b + ")");
   }
 
   /**
diff --git a/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nFormatBottom.java b/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nFormatBottom.java
index 44637a30b819..941f4e61d7cd 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nFormatBottom.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/i18nformatter/qual/I18nFormatBottom.java
@@ -22,5 +22,5 @@
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @SubtypeOf({I18nFormat.class, I18nInvalidFormat.class, I18nFormatFor.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface I18nFormatBottom {}
diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
index 11990235099e..3fecd1d288b1 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/IndexOrHigh.java
@@ -33,6 +33,11 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 public @interface IndexOrHigh {
-  /** The annotated expression is a valid index for, or is equal to the length of, each sequence. */
+  /**
+   * The annotated expression is a valid index for, or is equal to the length of, each sequence.
+   *
+   * @return sequences that the annotated expression is a valid index for or is equal to the length
+   *     of
+   */
   String[] value();
 }
diff --git a/src/java.base/share/classes/org/checkerframework/checker/index/qual/LengthOf.java b/src/java.base/share/classes/org/checkerframework/checker/index/qual/LengthOf.java
index 53adb1af1d4a..980d9796c8a0 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/index/qual/LengthOf.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/index/qual/LengthOf.java
@@ -13,7 +13,7 @@
  * detail that may change in the future, when this type may be used to implement more precise
  * refinements.
  *
- * <p>The usual use case for the {@code LengthOf} annotation is in the defintions of custom
+ * <p>The usual use case for the {@code LengthOf} annotation is in the definitions of custom
  * collections. Consider the signature of java.lang.String#length():
  *
  * <pre>
diff --git a/src/java.base/share/classes/org/checkerframework/checker/interning/qual/InternedDistinct.java b/src/java.base/share/classes/org/checkerframework/checker/interning/qual/InternedDistinct.java
index c1e7fb54a8cb..80b80e37cfaf 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/interning/qual/InternedDistinct.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/interning/qual/InternedDistinct.java
@@ -25,5 +25,5 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf(Interned.class)
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface InternedDistinct {}
diff --git a/src/java.base/share/classes/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java b/src/java.base/share/classes/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java
index af97ce2509f8..56be2b326f4d 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java
@@ -71,7 +71,7 @@
   /**
    * A wrapper annotation that makes the {@link EnsuresNonEmptyIf} annotation repeatable.
    *
-   * <p>Programmers generally do not need to write ths. It is created by Java when a programmer
+   * <p>Programmers generally do not need to write this. It is created by Java when a programmer
    * writes more than one {@link EnsuresNonEmptyIf} annotation at the same location.
    */
   @Retention(RetentionPolicy.RUNTIME)
diff --git a/src/java.base/share/classes/org/checkerframework/checker/optional/qual/RequiresPresent.java b/src/java.base/share/classes/org/checkerframework/checker/optional/qual/RequiresPresent.java
index d8754d3beacb..1ad847e9e0ae 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/optional/qual/RequiresPresent.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/optional/qual/RequiresPresent.java
@@ -63,7 +63,7 @@
 public @interface RequiresPresent {
 
   /**
-   * The Java expressions that that need to be {@link Present}.
+   * The Java expressions that need to be {@link Present}.
    *
    * @return the Java expressions that need to be {@link Present}
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
diff --git a/src/java.base/share/classes/org/checkerframework/checker/regex/qual/RegexBottom.java b/src/java.base/share/classes/org/checkerframework/checker/regex/qual/RegexBottom.java
index 2ffcb62ad718..b948170765bd 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/regex/qual/RegexBottom.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/regex/qual/RegexBottom.java
@@ -23,5 +23,5 @@
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @InvisibleQualifier
 @SubtypeOf({Regex.class, PartialRegex.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface RegexBottom {}
diff --git a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/BinaryName.java b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/BinaryName.java
index c178d9371fff..72e3272bdc50 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/BinaryName.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/BinaryName.java
@@ -9,7 +9,7 @@
 
 /**
  * Represents a binary name as defined in the <a
- * href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">Java Language
+ * href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">Java Language
  * Specification, section 13.1</a>.
  *
  * <p>For example, in
diff --git a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/CanonicalName.java b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/CanonicalName.java
index b22307594d81..946f216518d2 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/CanonicalName.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/CanonicalName.java
@@ -12,11 +12,10 @@
  * Every canonical name is a fully-qualified name, but not every fully-qualified name is a canonical
  * name.
  *
- * <p><a href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-6.html#jls-6.7">JLS section
+ * <p><a href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-6.html#jls-6.7">JLS section
  * 6.7</a> gives the following example:
  *
  * <blockquote>
- *
  * The difference between a fully qualified name and a canonical name can be seen in code such as:
  *
  * <pre>{@code
@@ -27,7 +26,6 @@
  *
  * Both {@code p.O1.I} and {@code p.O2.I} are fully qualified names that denote the member class
  * {@code I}, but only {@code p.O1.I} is its canonical name.
- *
  * </blockquote>
  *
  * Given a character sequence that is a fully-qualified name, there is no way to know whether or not
diff --git a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/FullyQualifiedName.java b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/FullyQualifiedName.java
index 9ed69097a969..6d2fcd7b7c5c 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/signature/qual/FullyQualifiedName.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/signature/qual/FullyQualifiedName.java
@@ -10,7 +10,7 @@
 /**
  * A sequence of dot-separated identifiers, followed by any number of array square brackets.
  * Represents a fully-qualified name as defined in the <a
- * href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-6.html#jls-6.7">Java Language
+ * href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-6.html#jls-6.7">Java Language
  * Specification, section 6.7</a>.
  *
  * <p>Examples:
diff --git a/src/java.base/share/classes/org/checkerframework/checker/sqlquotes/qual/SqlQuotesBottom.java b/src/java.base/share/classes/org/checkerframework/checker/sqlquotes/qual/SqlQuotesBottom.java
index 41acaca1641d..542f2a288119 100644
--- a/src/java.base/share/classes/org/checkerframework/checker/sqlquotes/qual/SqlQuotesBottom.java
+++ b/src/java.base/share/classes/org/checkerframework/checker/sqlquotes/qual/SqlQuotesBottom.java
@@ -23,5 +23,5 @@
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
 @InvisibleQualifier
 @SubtypeOf({SqlEvenQuotes.class, SqlOddQuotes.class})
-@DefaultFor(value = {TypeUseLocation.LOWER_BOUND})
+@DefaultFor({TypeUseLocation.LOWER_BOUND})
 public @interface SqlQuotesBottom {}
diff --git a/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/NonLeaked.java b/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/NonLeaked.java
index ad0b07366d57..5686d79b5b3d 100644
--- a/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/NonLeaked.java
+++ b/src/java.base/share/classes/org/checkerframework/common/aliasing/qual/NonLeaked.java
@@ -21,7 +21,7 @@
  */
 
 // This is a type qualifier because of a Checker Framework limitation (Issue 383), but its hierarchy
-// is ignored. Once the stub parser gets updated to read non-type-qualifiers annotations on stub
+// is ignored. Once the stub parser gets updated to store non-type-qualifier annotations from stub
 // files, this annotation won't be a type qualifier anymore.
 
 @Documented
diff --git a/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassBound.java b/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassBound.java
index 0cae3ff79e33..45bf1d9b9740 100644
--- a/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassBound.java
+++ b/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassBound.java
@@ -19,7 +19,7 @@
 @SubtypeOf({UnknownClass.class})
 public @interface ClassBound {
   /**
-   * The <a href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">binary
+   * The <a href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">binary
    * name</a> of the class or classes that upper-bound the values of this Class object.
    */
   String[] value();
diff --git a/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassVal.java b/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassVal.java
index 424efe40bb8f..a6d22b0bc4ce 100644
--- a/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassVal.java
+++ b/src/java.base/share/classes/org/checkerframework/common/reflection/qual/ClassVal.java
@@ -22,7 +22,7 @@
   /**
    * The name of the type that this Class object represents. The name is a "fully-qualified binary
    * name" ({@link org.checkerframework.checker.signature.qual.FqBinaryName}): a primitive or <a
-   * href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">binary name</a>,
+   * href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">binary name</a>,
    * possibly followed by some number of array brackets.
    *
    * @return the name of the type that this Class object represents
diff --git a/src/java.base/share/classes/org/checkerframework/common/reflection/qual/MethodVal.java b/src/java.base/share/classes/org/checkerframework/common/reflection/qual/MethodVal.java
index 3c7612321b0c..792119ad09e7 100644
--- a/src/java.base/share/classes/org/checkerframework/common/reflection/qual/MethodVal.java
+++ b/src/java.base/share/classes/org/checkerframework/common/reflection/qual/MethodVal.java
@@ -24,7 +24,7 @@
 @SubtypeOf({UnknownMethod.class})
 public @interface MethodVal {
   /**
-   * The <a href="https://docs.oracle.com/javase/specs/jls/se17/html/jls-13.html#jls-13.1">binary
+   * The <a href="https://docs.oracle.com/javase/specs/jls/se25/html/jls-13.html#jls-13.1">binary
    * name</a> of the class that declares this method.
    */
   String[] className();
diff --git a/src/java.base/share/classes/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java b/src/java.base/share/classes/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java
index 7ada21419f1e..70b38d5de7c1 100644
--- a/src/java.base/share/classes/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java
+++ b/src/java.base/share/classes/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java
@@ -23,6 +23,6 @@
 @SubtypeOf({})
 @DefaultQualifierInHierarchy
 @QualifierForLiterals(LiteralKind.NULL)
-@DefaultFor(value = TypeUseLocation.LOWER_BOUND)
+@DefaultFor(TypeUseLocation.LOWER_BOUND)
 @InvisibleQualifier
 public @interface UnknownThis {}
diff --git a/src/java.base/share/classes/org/checkerframework/dataflow/qual/Pure.java b/src/java.base/share/classes/org/checkerframework/dataflow/qual/Pure.java
index 82cdb5968795..3409465840f4 100644
--- a/src/java.base/share/classes/org/checkerframework/dataflow/qual/Pure.java
+++ b/src/java.base/share/classes/org/checkerframework/dataflow/qual/Pure.java
@@ -25,13 +25,4 @@
 @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
-  }
-}
+public @interface Pure {}
diff --git a/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectFree.java b/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectFree.java
index da33d80443e7..db55f24f792b 100644
--- a/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectFree.java
+++ b/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectFree.java
@@ -12,8 +12,8 @@
  *
  * <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.
+ * objects. A constructor is side-effect-free if it does not modify any objects that existed before
+ * it was called in ways that are externally visible.
  *
  * <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
diff --git a/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectsOnly.java b/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectsOnly.java
index ab6a7dd1718f..cb06cb25f51d 100644
--- a/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectsOnly.java
+++ b/src/java.base/share/classes/org/checkerframework/dataflow/qual/SideEffectsOnly.java
@@ -8,12 +8,27 @@
 import org.checkerframework.framework.qual.JavaExpression;
 
 /**
- * A method annotated with the declaration annotation {@code @SideEffectsOnly("A", "B")} changes the
- * value of at most the expressions A and B. All other expressions have the same value before and
- * after a call to the method.
+ * A method annotated with the declaration annotation {@code @SideEffectsOnly({"A", "B"})} changes
+ * the value of at most the expressions A and B. No other expression is directly modified by the
+ * method. Absent aliasing, no other expression has a different value after a call to the method.
+ * But checking of this annotation (under {@code -AcheckPurityAnnotations}) treats two expressions
+ * as possibly aliased only when an assignment relating them appears in the method body.
  *
- * @checker_framework.manual #type-refinement-purity Specifying side effects
+ * <p>This annotation is inherited by subtypes, just as if it were meta-annotated with
+ * {@code @InheritedAnnotation}.
+ *
+ * <p>On a constructor, this annotation constrains what the constructor modifies besides the object
+ * being constructed. Assigning to the new object's own fields is always permitted and need not be
+ * listed, because the object did not exist before the call; writing {@code this} in the annotation
+ * is legal but has no additional effect. At a {@code new} expression, the expressions that are
+ * reached through {@code this} are ignored, because the object being constructed did not exist
+ * before the call. A constructor's annotation does not yet affect type refinement at {@code new}
+ * expressions.
+ *
+ * @checker_framework.manual #side-effects-only-checking Checking {@code @SideEffectsOnly}
  */
+// @InheritedAnnotation cannot be written here, because "dataflow" project cannot depend on
+// "framework" project.
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@@ -21,9 +36,16 @@
   /**
    * An upper bound on the expressions that this method might change the value of.
    *
+   * <p>Each expression must denote the same location every time it is evaluated: it must be a
+   * variable, a field access, an array access, a literal, a class name, or a call to a {@link Pure}
+   * method, recursively. A {@code @Pure} method returns the same value every time it is called with
+   * the same arguments, so a call to one qualifies so long as its receiver and its arguments do. An
+   * expression such as {@code "#1.getList()"}, where {@code getList} is not {@code @Pure}, may
+   * denote a different value each time it is evaluated, so no method body could satisfy it.
+   *
    * @return the Java expressions that the annotated method might side-effect
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
    */
   @JavaExpression
-  public String[] value();
+  String[] value();
 }
diff --git a/src/java.base/share/classes/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java b/src/java.base/share/classes/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java
index 9b7feb69237b..0a158a141c1f 100644
--- a/src/java.base/share/classes/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java
+++ b/src/java.base/share/classes/org/checkerframework/framework/qual/ConditionalPostconditionAnnotation.java
@@ -37,11 +37,12 @@
  * <pre><code>
  * {@literal @}ConditionalPostconditionAnnotation(qualifier = MinLen.class)
  * {@literal @}Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
- * public {@literal @}interface EnsuresMinLen {
+ * public {@literal @}interface EnsuresMinLenIf {
  *   String[] expression();
  *   boolean result();
  *   {@literal @}QualifierArgument("value")
  *   int targetValue() default 0;
+ * }
  * </code></pre>
  *
  * The {@code expression} element holds the expressions to which the qualifier applies and {@code
@@ -52,7 +53,7 @@
  * {@code @MinLen(4)} upon returning {@code true}.
  *
  * <pre><code>
- * {@literal @}EnsuresMinLenIf(expression = "field", result = true, targetValue = 4")
+ * {@literal @}EnsuresMinLenIf(expression = "field", result = true, targetValue = 4)
  * public boolean isFieldBool() {
  *   return field == "true" || field == "false";
  * }
diff --git a/src/java.base/share/classes/org/checkerframework/framework/qual/DoesNotUnrefineReceiver.java b/src/java.base/share/classes/org/checkerframework/framework/qual/DoesNotUnrefineReceiver.java
index 4eca89c86484..33e94710d019 100644
--- a/src/java.base/share/classes/org/checkerframework/framework/qual/DoesNotUnrefineReceiver.java
+++ b/src/java.base/share/classes/org/checkerframework/framework/qual/DoesNotUnrefineReceiver.java
@@ -15,9 +15,8 @@
  * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and
  *     flow-sensitive analysis
  */
-// @InheritedAnnotation cannot be written here, because "dataflow" project cannot depend on
-// "framework" project.
 @Documented
+@InheritedAnnotation
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 public @interface DoesNotUnrefineReceiver {