Merge branch 'typetools:master' into bugfix/wpi-loop-unknowninitialization

Author: erfan-arvan

build.gradle

@@ -55,7 +55,7 @@ ext {
   versions = [
     autoValue       : '1.11.0',
     googleJavaFormat : '1.19.2',
-    lombok          : '1.18.32',
+    lombok          : '1.18.34',
     hashmapUtil : '0.0.1',
     reflectionUtil : '1.1.3',
     plumeUtil : '1.9.3',

framework/build.gradle

@@ -31,7 +31,7 @@ configurations {
 dependencies {
   api project(':javacutil')
   api project(':dataflow')
-  api 'org.checkerframework:stubparser:3.25.10'
+  api 'org.checkerframework:stubparser:3.26.1'
   // AFU is an "includedBuild" imported in checker-framework/settings.gradle, so the version number doesn't matter.
   // https://docs.gradle.org/current/userguide/composite_builds.html#settings_defined_composite
   api('org.checkerframework:annotation-file-utilities:*') {

framework/src/main/java/org/checkerframework/framework/ajava/InsertAjavaAnnotations.java

@@ -1,6 +1,9 @@
 package org.checkerframework.framework.ajava;
 
+import com.github.javaparser.JavaToken;
+import com.github.javaparser.JavaToken.Kind;
 import com.github.javaparser.Position;
+import com.github.javaparser.TokenRange;
 import com.github.javaparser.ast.CompilationUnit;
 import com.github.javaparser.ast.ImportDeclaration;
 import com.github.javaparser.ast.Node;
@@ -11,6 +14,7 @@
 import com.github.javaparser.ast.expr.AnnotationExpr;
 import com.github.javaparser.ast.nodeTypes.NodeWithAnnotations;
 import com.github.javaparser.ast.type.ArrayType;
+import com.github.javaparser.ast.type.ArrayType.ArrayBracketPair;
 import com.github.javaparser.ast.type.ClassOrInterfaceType;
 import com.github.javaparser.ast.type.Type;
 import com.github.javaparser.printer.DefaultPrettyPrinter;
@@ -238,23 +242,29 @@ public void defaultAction(Node src, Node dest) {
     @Override
     public void visit(ArrayType src, Node other) {
       ArrayType dest = (ArrayType) other;
-      // The second component of this pair contains a list of ArrayBracketPairs from left to
-      // right. For example, if src contains String[][], then the list will contain the
-      // types String[] and String[][]. To insert array annotations in the correct location,
-      // we insert them directly to the right of the end of the previous element.
-      Pair<Type, List<ArrayType.ArrayBracketPair>> srcArrayTypes = ArrayType.unwrapArrayTypes(src);
-      Pair<Type, List<ArrayType.ArrayBracketPair>> destArrayTypes =
-          ArrayType.unwrapArrayTypes(dest);
-      // The first annotations go directly after the element type.
-      Position firstPosition = destArrayTypes.a.getEnd().get();
-      addAnnotations(firstPosition, srcArrayTypes.b.get(0).getAnnotations(), 1, false);
-      for (int i = 1; i < srcArrayTypes.b.size(); i++) {
-        Position position = destArrayTypes.b.get(i - 1).getTokenRange().get().toRange().get().end;
-        addAnnotations(position, srcArrayTypes.b.get(i).getAnnotations(), 1, true);
+      Pair<Type, List<ArrayBracketPair>> destArrayTypes = ArrayType.unwrapArrayTypes(dest);
+      TokenRange innerMostCom = destArrayTypes.a.getTokenRange().get();
+
+      List<Position> positions = new ArrayList<>();
+      for (JavaToken token : dest.getTokenRange().get().withBegin(innerMostCom.getEnd())) {
+        if (token.getKind() == Kind.LBRACKET.getKind()) {
+          positions.add(token.getRange().get().begin);
+        }
+      }
+
+      // At the end of the loop, these two variables will contain the innermost array type.
+      ArrayType srcArray = src;
+      ArrayType destArray = dest;
+      for (Position position : positions) {
+        addAnnotations(position, srcArray.getAnnotations(), 0, true);
+        if (srcArray.getComponentType().isArrayType()) {
+          srcArray = (ArrayType) srcArray.getComponentType();
+          destArray = (ArrayType) destArray.getComponentType();
+        }
       }
 
-      // Visit the component type.
-      srcArrayTypes.a.accept(this, destArrayTypes.a);
+      // Visit the innermost component type.
+      srcArray.getComponentType().accept(this, destArray.getComponentType());
     }
 
     @Override

framework/src/main/java/org/checkerframework/framework/ajava/JointJavacJavaParserVisitor.java

@@ -45,6 +45,7 @@
 import com.github.javaparser.ast.expr.SwitchExpr;
 import com.github.javaparser.ast.expr.ThisExpr;
 import com.github.javaparser.ast.expr.TypeExpr;
+import com.github.javaparser.ast.expr.TypePatternExpr;
 import com.github.javaparser.ast.expr.UnaryExpr;
 import com.github.javaparser.ast.modules.ModuleDeclaration;
 import com.github.javaparser.ast.modules.ModuleExportsDirective;
@@ -284,7 +285,7 @@ public Void visitBinary(BinaryTree javacTree, Node javaParserNode) {
    */
   @SuppressWarnings("UnusedVariable")
   public Void visitBindingPattern17(Tree javacTree, Node javaParserNode) {
-    PatternExpr patternExpr = castNode(PatternExpr.class, javaParserNode, javacTree);
+    TypePatternExpr patternExpr = castNode(TypePatternExpr.class, javaParserNode, javacTree);
     processBindingPattern(javacTree, patternExpr);
     VariableTree variableTree = BindingPatternUtils.getVariable(javacTree);
     // The name expression can be null, even when a name exists.

framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java

@@ -37,10 +37,7 @@ public class JavaParserUtil {
    * The Language Level to use when parsing if a specific level isn't applied. This should be the
    * highest version of Java that the Checker Framework can process.
    */
-  // JavaParser's ParserConfiguration.LanguageLevel has no constant for JDK 18, as of version
-  // 3.25.1 (2023-02-28).  See
-  // https://www.javadoc.io/doc/com.github.javaparser/javaparser-core/latest/com/github/javaparser/ParserConfiguration.LanguageLevel.html .
-  public static final LanguageLevel DEFAULT_LANGUAGE_LEVEL = LanguageLevel.JAVA_17;
+  public static final LanguageLevel DEFAULT_LANGUAGE_LEVEL = LanguageLevel.JAVA_21;
 
   ///
   /// Replacements for StaticJavaParser

framework/tests/all-systems/java17/Figure.java

@@ -0,0 +1,29 @@
+// @below-java17-jdk-skip-test
+// @infer-jaifs-skip-test
+// from https://docs.oracle.com/en/java/javase/15/language/sealed-classes-and-interfaces.html
+
+public sealed class Figure
+// The permits clause has been omitted
+// as its permitted classes have been
+// defined in the same file.
+{}
+
+@SuppressWarnings("initializedfields:contracts.postcondition")
+final class Circle extends Figure {
+  float radius;
+}
+
+@SuppressWarnings("initializedfields:contracts.postcondition")
+non-sealed class Square extends Figure {
+  float side;
+}
+
+@SuppressWarnings("initializedfields:contracts.postcondition")
+sealed class Rectangle extends Figure {
+  float length, width;
+}
+
+@SuppressWarnings("initializedfields:contracts.postcondition")
+final class FilledRectangle extends Rectangle {
+  int red, green, blue, sealed;
+}