Merge branch 'master' into RDM-test

.github/workflows/ci.yml

@@ -64,12 +64,20 @@ jobs:
       fail-fast: true
       matrix:
         # No need to run 'cftests-junit-jdk21' on JDK 21.
-        script: ['typecheck-part1', 'typecheck-part2', 'guava', 'plume-lib', 'daikon-part1', 'daikon-part2', 'jspecify-conformance', 'jspecify-reference-checker']
+        script: ['typecheck-part1', 'typecheck-part2', 'guava', 'plume-lib', 'daikon-part1', 'daikon-part2', 'jspecify-conformance', 'jspecify-reference-checker', 'misc']
         java_version: [21]
     env:
       JAVA_VERSION: ${{ matrix.java_version }}
     steps:
     - uses: actions/checkout@v4
+      if: matrix.script != 'misc'
+      with:
+        fetch-depth: 1
+    - uses: actions/checkout@v4
+      if: matrix.script == 'misc'
+      with:
+        # CI diff needs more history - 0 fetches all history.
+        fetch-depth: 0
     - name: Set up JDK ${{ matrix.java_version }}
       uses: actions/setup-java@v4
       with:
@@ -80,7 +88,17 @@ jobs:
     # See: https://github.com/gradle/actions/blob/main/setup-gradle/README.md
     - name: Setup Gradle
       uses: gradle/actions/setup-gradle@v4.2.2
-
+      # Setup for misc tests
+    - name: Install misc dependencies
+      if: matrix.script == 'misc'
+      run: |
+        sudo apt install -y shellcheck devscripts python3-pip \
+          texlive-latex-base texlive-latex-extra latexmk librsvg2-bin \
+          autoconf dia hevea latexmk libasound2-dev rsync pdf2svg \
+          libcups2-dev libfontconfig1-dev libx11-dev libxext-dev \
+          libxrender-dev libxrandr-dev libxtst-dev libxt-dev \
+          texlive-font-utils texlive-fonts-recommended texlive-latex-recommended
+        pip install black flake8 html5validator
     - name: Run test script checker/bin-devel/test-${{ matrix.script }}
       run: ./checker/bin-devel/test-${{ matrix.script }}.sh
 
@@ -94,19 +112,26 @@ jobs:
       fail-fast: true
       matrix:
         # jspecify-conformance and jspecify-reference-checker only tested on JDK 21.
-        script: ['cftests-junit', 'cftests-nonjunit', 'cftests-junit-jdk21', 'typecheck-part1', 'typecheck-part2', 'guava', 'plume-lib', 'daikon-part1', 'daikon-part2']
+        script: ['cftests-junit', 'cftests-nonjunit', 'cftests-junit-jdk21', 'typecheck-part1', 'typecheck-part2', 'guava', 'plume-lib', 'daikon-part1', 'daikon-part2', 'misc']
         # JDK 21 used by sanity before
         java: [{version: '8', experimental: false},
           {version: '11', experimental: false},
           {version: '17', experimental: false},
-          {version: '22', experimental: true},
-          {version: '23-ea', experimental: true},
+          {version: '23', experimental: false},
           {version: '24-ea', experimental: true}]
     env:
       JAVA_VERSION: ${{ matrix.java.version }}
     continue-on-error: ${{ matrix.java.experimental }}
     steps:
     - uses: actions/checkout@v4
+      if: matrix.script != 'misc'
+      with:
+        fetch-depth: 1
+    - uses: actions/checkout@v4
+      if: matrix.script == 'misc'
+      with:
+        # CI diff needs more history - 0 fetches all history.
+        fetch-depth: 0
     - name: Set up JDK ${{ matrix.java.version }}
       uses: actions/setup-java@v4
       with:
@@ -125,7 +150,17 @@ jobs:
     # See: https://github.com/gradle/actions/blob/main/setup-gradle/README.md
     - name: Setup Gradle
       uses: gradle/actions/setup-gradle@v4.2.2
-
+    # Setup for misc tests
+    - name: Install misc dependencies
+      if: matrix.script == 'misc'
+      run: |
+        sudo apt install -y shellcheck devscripts python3-pip \
+          texlive-latex-base texlive-latex-extra latexmk librsvg2-bin \
+          autoconf dia hevea latexmk libasound2-dev rsync pdf2svg \
+          libcups2-dev libfontconfig1-dev libx11-dev libxext-dev \
+          libxrender-dev libxrandr-dev libxtst-dev libxt-dev \
+          texlive-font-utils texlive-fonts-recommended texlive-latex-recommended
+        pip install black flake8 html5validator
     - name: Setup Bazel
       uses: bazel-contrib/setup-bazel@0.10.0
       if: matrix.script == 'cftests-nonjunit'

build.gradle

@@ -51,8 +51,9 @@ ext {
     // The int corresponding to the major version of the current JVM.
     currentRuntimeJavaVersion = majorVersionToInt(JavaVersion.current().getMajorVersion())
 
-    // As of 2024-08-06, delombok doesn't yet support JDK 23; see https://projectlombok.org/changelog .
-    skipDelombok = currentRuntimeJavaVersion >= 23
+    // As of 2024-12-24, delombok doesn't yet support JDK 24; see https://projectlombok.org/changelog .
+    // Keep in sync with check in docs/examples/lombok/Makefile
+    skipDelombok = currentRuntimeJavaVersion >= 24
 
     parentDir = file("${rootDir}/../").absolutePath
 

checker/build.gradle

@@ -80,7 +80,7 @@ dependencies {
     testImplementation 'com.amazonaws:aws-java-sdk-ec2'
     testImplementation 'com.amazonaws:aws-java-sdk-kms'
     // The AWS SDK is used for testing the Called Methods Checker.
-    testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.770')
+    testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.780')
     // For the Resource Leak Checker's support for JavaEE.
     testImplementation 'javax.servlet:javax.servlet-api:4.0.1'
     // For the Resource Leak Checker's support for IOUtils.

checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java

@@ -170,9 +170,9 @@ protected boolean commonAssignmentCheck(
             }
         }
 
-        /// TODO: What does "take precedence over" mean?  Both are issued, but the
-        /// "i18nformat.excess.arguments" appears first in the output.  Is this meant to not call
-        /// super.commonAssignmentCheck() if `result` is already false?
+        // TODO: What does "take precedence over" mean?  Both are issued, but the
+        // "i18nformat.excess.arguments" appears first in the output.  Is this meant to not call
+        // super.commonAssignmentCheck() if `result` is already false?
         // By calling super.commonAssignmentCheck() last, any "i18nformat.excess.arguments"
         // message issued for a given line of code will take precedence over the
         // "assignment.type.incompatible"

checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundTransfer.java

@@ -175,10 +175,16 @@ public TransferResult<CFValue, CFStore> visitAssignment(
      * {@code node} is known to be {@code typeOfNode}. If the node is a plus or a minus then the
      * types of the left and right operands can be refined to include offsets. If the node is a
      * multiplication, its operands can also be refined. See {@link
-     * #propagateToAdditionOperand(LessThanLengthOf, Node, Node, TransferInput, CFStore)}, {@link
-     * #propagateToSubtractionOperands(LessThanLengthOf, NumericalSubtractionNode, TransferInput,
-     * CFStore)}, and {@link #propagateToMultiplicationOperand(LessThanLengthOf, Node, Node,
-     * TransferInput, CFStore)} for details.
+     * #propagateToAdditionOperand(UBQualifier.LessThanLengthOf, Node, Node, TransferInput,
+     * CFStore)}, {@link #propagateToSubtractionOperands(UBQualifier.LessThanLengthOf,
+     * NumericalSubtractionNode, TransferInput, CFStore)}, and {@link
+     * #propagateToMultiplicationOperand(UBQualifier.LessThanLengthOf, Node, Node, TransferInput,
+     * CFStore)} for details.
+     *
+     * @param typeOfNode type of node
+     * @param node the node
+     * @param in the TransferInput before propagate to this operand
+     * @param store location to store the refined type
      */
     private void propagateToOperands(
             LessThanLengthOf typeOfNode,
@@ -234,10 +240,10 @@ private void propagateToMultiplicationOperand(
      *
      * <p>This means that the left node is less than or equal to the length of the array when the
      * right node is subtracted from the left node. Note that unlike {@link
-     * #propagateToAdditionOperand(LessThanLengthOf, Node, Node, TransferInput, CFStore)} and {@link
-     * #propagateToMultiplicationOperand(LessThanLengthOf, Node, Node, TransferInput, CFStore)},
-     * this method takes the NumericalSubtractionNode instead of the two operand nodes. This
-     * implements case 4.
+     * #propagateToAdditionOperand(UBQualifier.LessThanLengthOf, Node, Node, TransferInput,
+     * CFStore)} and {@link #propagateToMultiplicationOperand(UBQualifier.LessThanLengthOf, Node,
+     * Node, TransferInput, CFStore)}, this method takes the NumericalSubtractionNode instead of the
+     * two operand nodes. This implements case 4.
      *
      * @param typeOfSubtraction type of node
      * @param node subtraction node that has typeOfSubtraction

checker/src/test/java/org/checkerframework/checker/test/junit/AnnotatedForNullnessTest.java

@@ -28,6 +28,9 @@ public AnnotatedForNullnessTest(List<File> testFiles) {
      */
     @Parameters
     public static String[] getTestDirs() {
-        return new String[] {"nulless-conservative-defaults/annotatedfornullness"};
+        return new String[] {
+            "nulless-conservative-defaults/annotatedfornullness",
+            "nulless-conservative-defaults/packageannotatedfornullness"
+        };
     }
 }

checker/tests/i18n-formatter/Syntax.java

@@ -83,8 +83,11 @@ public static void invalidSubformatPattern() {
         MessageFormat.format("{0, number, #.#.#}", 1);
         // :: error: (i18nformat.string.invalid)
         MessageFormat.format("{0, date, y.m.d.x}", new Date());
-        // :: error: (i18nformat.string.invalid)
-        MessageFormat.format("{0, choice, 0##zero}", 0);
+
+        // TODO: This pattern is valid starting with JDK 23. Decide how to handle version-specific
+        // issues.
+        // TODO :: error: (i18nformat.string.invalid)
+        // MessageFormat.format("{0, choice, 0##zero}", 0);
 
         // good
         MessageFormat.format("{0, number, #.#}", 1);

checker/tests/nulless-conservative-defaults/packageannotatedfornullness/annotated/Test.java

@@ -0,0 +1,10 @@
+package packageannotatedfornullness.annotated;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class Test {
+    void foo(@Nullable Object o) {
+        // :: error: (dereference.of.nullable)
+        o.toString();
+    }
+}

checker/tests/nulless-conservative-defaults/packageannotatedfornullness/annotated/package-info.java

@@ -0,0 +1,4 @@
+@AnnotatedFor("nullness")
+package packageannotatedfornullness.annotated;
+
+import org.checkerframework.framework.qual.AnnotatedFor;

checker/tests/nulless-conservative-defaults/packageannotatedfornullness/notannotated/Test.java

@@ -0,0 +1,10 @@
+package packageannotatedfornullness.notannotated;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class Test {
+    void foo(@Nullable Object o) {
+        // No error because this package is not annotated for nullness.
+        o.toString();
+    }
+}

checker/tests/nulless-conservative-defaults/packageannotatedfornullness/notannotated/package-info.java

@@ -0,0 +1 @@
+package packageannotatedfornullness.notannotated;

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/UnconditionalJump.java

@@ -52,7 +52,7 @@ public FlowRule getFlowRule() {
      * Produce a string representation.
      *
      * @return a string representation
-     * @see org.checkerframework.dataflow.cfg.builder.CFGBuilder.PhaseOneResult#nodeToString
+     * @see org.checkerframework.dataflow.cfg.builder.PhaseOneResult#nodeToString
      */
     @Override
     public String toString() {

docs/CHANGELOG.md

@@ -7,6 +7,8 @@ Version 3.42.0-eisop6 (January ??, 2025)
 
 **Closed issues:**
 
+eisop#1033.
+
 
 Version 3.42.0-eisop5 (December 20, 2024)
 -----------------------------------------

docs/examples/BazelExample/MODULE.bazel

@@ -1,4 +1,4 @@
-bazel_dep(name = "rules_jvm_external", version = "6.2")
+bazel_dep(name = "rules_jvm_external", version = "6.6")
 maven = use_extension("@rules_jvm_external//:extensions.bzl", "maven")
 maven.install(
     artifacts = [

docs/examples/BazelExample/Makefile

@@ -1,8 +1,15 @@
+JAVA_VER := $(shell java -version 2>&1 | head -1 | cut -d'"' -f2 | sed '/^1\./s///' | cut -d'.' -f1 | sed 's/-ea//')
+
 .PHONY: all clean
 
+ifeq ($(shell test $(JAVA_VER) -gt 21; echo $$?),0)
+all:
+	@echo "Skipping test because I don't know how to configure bazel to work on a JDK > 21..."
+else
 all:
 	bazelisk run example > Out.txt 2>&1 || true
 	grep -qF "BazelExample.java:25: error: [assignment.type.incompatible] incompatible types in assignment." Out.txt || (echo "FAILURE.  Here is file Out.txt:" && cat Out.txt && echo "End of file Out.txt." && false)
+endif
 
 clean:
 	-bazelisk clean

docs/examples/lombok/Makefile

@@ -4,8 +4,8 @@ JAVA_VER := $(shell java -version 2>&1 | head -1 | cut -d'"' -f2 | sed '/^1\./s/
 
 # Delomboking seems to mess up line numbers. The actual error is on line 13, but the error appears on line 12.
 # So check for both the error message and make sure it is for the right assignment.
-# As of 2023-09-23, lombok does not work under Java 22, see https://projectlombok.org/changelog .
-ifeq (${JAVA_VER},22)
+# As of 2024-12-24, lombok does not work under Java 24, see https://projectlombok.org/changelog .
+ifeq ($(shell test $(JAVA_VER) -gt 23; echo $$?),0)
 all:
 	@echo "Skipping test because lombok does not work under Java ${JAVA_VER}"
 else

docs/manual/creating-a-checker.tex

@@ -212,7 +212,7 @@
 repository \url{https://github.com/eisop/checker-framework}.
 Another choice is to write it in a stand-alone repository.  Here is a
 template for a stand-alone repository:
-\url{https://github.com/typetools/templatefora-checker}; at that URL,
+\url{https://github.com/eisop/templatefora-checker}; at that URL,
 click the ``Use this template'' button.
 
 % You may also wish to consult Section~\ref{creating-testing-framework} for