Add Modifiability Annotations

.azure/azure-pipelines.yml

@@ -16,6 +16,7 @@ jobs:
           pwd
           ls -al
           env | sort
+          set
         displayName: show environment
       - bash: pwd && ls && bash ./configure --with-jtreg=/usr/share/jtreg --disable-warnings-as-errors
         displayName: configure
@@ -41,6 +42,7 @@ jobs:
           pwd
           ls -al
           env | sort
+          set
         displayName: show environment
       - bash: |
           set -ex

.azure/azure-pipelines.yml.m4

@@ -19,6 +19,7 @@ jobs:
           pwd
           ls -al
           env | sort
+          set
         displayName: show environment
       - bash: pwd && ls && bash ./configure --with-jtreg=/usr/share/jtreg --disable-warnings-as-errors
         displayName: configure
@@ -44,6 +45,7 @@ jobs:
           pwd
           ls -al
           env | sort
+          set
         displayName: show environment
       - bash: |
           set -ex

.github/workflows/ci.yml

@@ -42,10 +42,7 @@ jobs:
           git config --get remote.origin.url || true
           pwd
           ls -al
-          echo "HOME=${HOME}"
-          echo "USER=${USER}"
-          echo "SHELL=${SHELL}"
-          echo "GITHUB_WORKSPACE=${GITHUB_WORKSPACE}"
+          set
       - name: configure
         run: |
           pwd
@@ -73,10 +70,7 @@ jobs:
           git config --get remote.origin.url || true
           pwd
           ls -al
-          echo "HOME=${HOME}"
-          echo "USER=${USER}"
-          echo "SHELL=${SHELL}"
-          echo "GITHUB_WORKSPACE=${GITHUB_WORKSPACE}"
+          set
       - name: clone git-scripts
         run: |
           set -ex
@@ -199,6 +193,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -218,6 +215,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -237,6 +237,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -256,6 +259,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -275,6 +281,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -294,6 +303,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -313,6 +325,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -332,6 +347,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -351,6 +369,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -370,6 +391,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -389,6 +413,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -408,6 +435,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -427,6 +457,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -446,6 +479,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -465,6 +501,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -484,6 +523,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -504,6 +546,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -523,6 +568,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -542,6 +590,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -561,6 +612,9 @@ jobs:
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework

.github/workflows/ci.yml.m4

@@ -46,10 +46,7 @@ jobs:
           git config --get remote.origin.url || true
           pwd
           ls -al
-          echo "HOME=${HOME}"
-          echo "USER=${USER}"
-          echo "SHELL=${SHELL}"
-          echo "GITHUB_WORKSPACE=${GITHUB_WORKSPACE}"
+          set
       - name: configure
         run: |
           pwd
@@ -77,10 +74,7 @@ jobs:
           git config --get remote.origin.url || true
           pwd
           ls -al
-          echo "HOME=${HOME}"
-          echo "USER=${USER}"
-          echo "SHELL=${SHELL}"
-          echo "GITHUB_WORKSPACE=${GITHUB_WORKSPACE}"
+          set
       - name: clone git-scripts
         run: |
           set -ex

.github/workflows/defs.m4

@@ -25,6 +25,9 @@ define([cftests_job], [dnl
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -46,6 +49,9 @@ define([daikon_job], [dnl
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework
@@ -66,6 +72,9 @@ define([plume_lib_job], [dnl
           fetch-depth: 25
           show-progress: false
           persist-credentials: false
+      - name: git config
+        run: |
+          git config --global --add safe.directory /__w/jdk/jdk
       - name: clone git-scripts
         run: mkdir -p /tmp/$USER && git -C /tmp/$USER clone --depth=1 -q https://github.com/plume-lib/git-scripts.git
       - name: clone checker-framework

README.md

@@ -141,19 +141,19 @@ To update that copy, run the command below from this directory:
 rm -f checker-qual.jar && \
 cp -p $CHECKERFRAMEWORK/checker-qual/build/libs/checker-qual-*-sources.jar checker-qual.jar && \
 (cd src/java.base/share/classes && rm -rf org/checkerframework && \
+  touch META-INF && \
   unzip ../../../../checker-qual.jar -x module-info.java -x 'META-INF*' && \
   rm -f org/checkerframework/checker/signedness/SignednessUtilExtra.java && \
   chmod -R u+w org/checkerframework) && \
 jar tf checker-qual.jar | grep '\.java$' | grep -v 'module-info.java' | sed 's/\/[^/]*\.java/;/' | sed 's/\//./g' | sed 's/^/    exports /' | sort -u
 ```
 
-The result of the command will be a list of export lines.
-Replace the existing export lines present in
-`src/java.base/share/classes/module-info.java` with the newly-generated list of
-exports. If no new packages were added, then likely no changes are needed
-in the `module-info.java` file.
+In addition to updating `.java` files, the command will output a list of export
+lines.  Place them in `src/java.base/share/classes/module-info.java`.  If no new
+packages were recently added to the Checker Framework, then likely no changes
+are needed in the `module-info.java` file.
 
-Commit the changes, including the new `checker.jar` file and any new `.java`
+Commit the changes, including the new `checker-qual.jar` file and any new `.java`
 files in a `qual/` directory.  (Both are used, by different parts of the build.)
 
 ## The typetools/jdk21u repository

src/java.base/share/classes/java/io/ObjectInputStream.java

@@ -4099,6 +4099,7 @@ void clear() {
         /**
          * Returns number of handles registered in table.
          */
+        @Pure
         int size() {
             return size;
         }
@@ -4148,6 +4149,7 @@ public int get(int index) {
                 return list[index];
             }
 
+            @Pure
             public int size() {
                 return size;
             }

src/java.base/share/classes/java/io/ObjectOutputStream.java

@@ -31,6 +31,7 @@
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signedness.qual.PolySigned;
+import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.framework.qual.AnnotatedFor;
 
 import java.security.AccessController;
@@ -2344,6 +2345,7 @@ void clear() {
         /**
          * Returns the number of mappings currently in table.
          */
+        @Pure
         int size() {
             return size;
         }
@@ -2444,6 +2446,7 @@ void clear() {
         /**
          * Returns the number of mappings currently in table.
          */
+        @Pure
         int size() {
             return htab.size();
         }

src/java.base/share/classes/java/lang/Iterable.java

@@ -25,6 +25,7 @@
 package java.lang;
 
 import org.checkerframework.checker.index.qual.PolyGrowShrink;
+import org.checkerframework.checker.modifiability.qual.MaybeModifiable;
 import org.checkerframework.checker.nonempty.qual.PolyNonEmpty;
 import org.checkerframework.common.aliasing.qual.NonLeaked;
 import org.checkerframework.framework.qual.AnnotatedFor;
@@ -51,7 +52,7 @@ public interface Iterable<T> {
      *
      * @return an Iterator.
      */
-    @PolyGrowShrink @PolyNonEmpty Iterator<T> iterator(@PolyGrowShrink @PolyNonEmpty Iterable<T> this);
+    @MaybeModifiable @PolyGrowShrink @PolyNonEmpty Iterator<T> iterator(@MaybeModifiable @PolyGrowShrink @PolyNonEmpty Iterable<T> this);
 
     /**
      * Performs the given action for each element of the {@code Iterable}