Merge branch 'main' into mulbrichPolymorphic

.github/workflows/code_quality.yml

@@ -24,21 +24,6 @@ jobs:
       - name: Build with Gradle
         run: ./gradlew -DENABLE_NULLNESS=true compileTest
 
-
-  qodana:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          fetch-depth: 0
-      - name: 'Qodana Scan'
-        uses: JetBrains/[email protected]
-
-      - uses: github/codeql-action/upload-sarif@v3
-        if: success() || failure()
-        with:
-          sarif_file: ${{ runner.temp }}/qodana/results/qodana.sarif.json
-
   formatting:
     runs-on: ubuntu-latest
     steps:
@@ -48,78 +33,5 @@ jobs:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-      - name: Setup Gradle
-        uses: gradle/actions/[email protected]
-      - name: SpotlessCheck
-        run: ./gradlew --continue spotlessCheck
-
-  # checkstyle:
-  #   runs-on: ubuntu-latest
-  #   steps:
-  #     - uses: actions/checkout@v4
-  #       with:
-  #         fetch-depth: 0
-  #     - run: scripts/tools/checkstyle/runIncrementalCheckstyle.sh --xml | tee report.xml
-  #     - run: |
-  #         npx violations-command-line -sarif sarif-report.json \
-  #         -v "CHECKSTYLE" "." ".*/report.xml$" "Checkstyle"     \
-  #         -diff-to $(git merge-base HEAD origin/main) -pv false
-
-  #     - uses: github/codeql-action/upload-sarif@v3
-  #       if: success() || failure()
-  #       with:
-  #         sarif_file: sarif-report.json
-
-
-  checkstyle_new:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-java@v4
-        with:
-          distribution: 'corretto'
-          java-version: '21'
-          cache: 'gradle'
-      - name: Setup Gradle
-        uses: gradle/actions/[email protected]
-      - name: Checkstyle
-        run: ./gradlew --continue checkstyleMainChanged
-      - run: |
-          npx violations-command-line -sarif sarif-report.json \
-          -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle"
-
-      #-diff-from $(git merge-base HEAD origin/main)
-      # - run: python3 ./.github/printcs.py */build/reports/checkstyle/main_diff.xml
-
-      # $(git merge-base HEAD origin/main)
-
-      - uses: github/codeql-action/upload-sarif@v3
-        if: success() || failure()
-        with:
-          sarif_file: sarif-report.json          
-
-  pmd:
-    runs-on: ubuntu-latest      
-    steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-java@v4
-        with:
-          distribution: 'corretto'
-          java-version: '21'
-          cache: 'gradle'
-      - name: Setup Gradle
-        uses: gradle/actions/[email protected]
-      - name: PMD checks
-        run: ./gradlew --continue pmdMainChanged
-
-      # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml
-
-      - run: |
-          npx violations-command-line -sarif pmd-report.json \
-          -v "PMD" "." ".*/build/reports/pmd/main_diff.xml$" "PMD"
-
-      # -diff-from $(git merge-base HEAD origin/main)
-      - name: Upload SARIF file
-        uses: github/codeql-action/upload-sarif@v3
-        with:
-          sarif_file: pmd-report.json
+      - name: Build with Gradle
+        run: ./gradlew --parallel --continue spotlessCheck

.github/workflows/sonarqube.yml

@@ -0,0 +1,49 @@
+## Copied from SonarCloud
+
+name: SonarCloud
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    types: [opened, synchronize, reopened]
+
+jobs:
+  build:
+    name: Build and analyze
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0  # Shallow clones should be disabled for a better relevancy of analysis
+      - name: Set up JDK 21
+        uses: actions/setup-java@v3
+        with:
+          java-version: 21
+          distribution: 'zulu' 
+      - name: Cache SonarCloud packages
+        uses: actions/cache@v3
+        with:
+          path: ~/.sonar/cache
+          key: ${{ runner.os }}-sonar
+          restore-keys: ${{ runner.os }}-sonar
+      - name: Cache Gradle packages
+        uses: actions/cache@v3
+        with:
+          path: ~/.gradle/caches
+          key: ${{ runner.os }}-gradle-${{ hashFiles('**/*.gradle') }}
+          restore-keys: ${{ runner.os }}-gradle
+
+      - name: Generate and submit dependency graph
+        uses: gradle/actions/dependency-submission@v3
+        with:
+            build-scan-publish: true
+            build-scan-terms-of-use-url: "https://gradle.com/terms-of-service"
+            build-scan-terms-of-use-agree: "yes"
+
+      - name: Build and analyze
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}  # Needed to get PR information, if any
+          SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}
+          GRADLE_OPTS: "-Xmx6g -XX:MaxMetaspaceSize=512m  -Dfile.encoding=UTF-8"
+        run: ./gradlew --parallel --continue  -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test classes testClasses :key.util:test jacocoTestReport sonar

build.gradle

@@ -25,8 +25,19 @@ plugins {
 
     // EISOP Checker Framework
     id "org.checkerframework" version "0.6.45"
+
+    id("org.sonarqube") version "5.0.0.4638"
+}
+
+sonar {
+  properties {
+    property "sonar.projectKey", "KeYProject_key"
+    property "sonar.organization", "keyproject"
+    property "sonar.host.url", "https://sonarcloud.io"
+  }
 }
 
+
 // Configure this project for use inside IntelliJ:
 idea {
     module {

gradle.properties

@@ -0,0 +1 @@
+org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8

key.core/src/main/antlr4/KeYLexer.g4

@@ -145,6 +145,7 @@ EQUAL_UNIQUE : '\\equalUnique';
 NEW : '\\new';
 NEW_TYPE_OF: '\\newTypeOf';
 NEW_DEPENDING_ON: '\\newDependingOn';
+NEW_LOCAL_VARS: '\\newLocalVars';
 HAS_ELEMENTARY_SORT:'\\hasElementarySort';
 NEWLABEL : '\\newLabel';
 CONTAINS_ASSIGNMENT : '\\containsAssignment';

key.core/src/main/antlr4/KeYParser.g4

@@ -707,6 +707,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
   | NEW
   | NEW_TYPE_OF
   | NEW_DEPENDING_ON
+  | NEW_LOCAL_VARS
   | HAS_ELEMENTARY_SORT
   | SAME
   | ISSUBTYPE

key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.visitor;
 
+
 import de.uka.ilkd.key.java.ProgramElement;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.SourceElement;
@@ -16,6 +17,7 @@
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
+
 /**
  * Walks through a java AST in depth-left-fist-order. This walker is used to transform a program
  * according to the given SVInstantiations.