Merge branch 'main' into eisop/keycore2

* main: (77 commits)
  Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
  spotless
  update oracle for taclet equality test
  change gradle github action to new syntax
  adding comments to jml spec factory default contracts
  repair soundness of assignment2UpdateRules with checked overflows
  spotless
  EQ version of seqSwapPreservesSeqPerm + proof
  added rule for sequences: swap preserves perm
  Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable
  spotlessing ...
  making RuleCommand work if already fully instantiated
  RuleCommand can now deal with rules that have schema variables for logical variables.
  Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof   obligation
  Code clean up (remove unused method)
  Fix loading of closed proofs (GUI threw error)
  Fix and test goToNext()
  Fix goToNextSibling() (thx Tobias)
  Format
  Add comments and next() method
  ...

.github/workflows/update_symbex_oracles.yml → .github/old_workflows/update_symbex_oracles.yml

@@ -16,16 +16,16 @@ jobs:
     runs-on: ubuntu-latest
     continue-on-error: true
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up JDK 21
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: '21'
           distribution: 'corretto'
           cache: 'gradle'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2
+        uses: gradle/gradle-build-action@v3
         with:
           arguments: --continue -D UPDATE_TEST_ORACLE=true -D ORACLE_DIRECTORY=key.core.symbolic_execution/src/test/resources/testcase :key.core.symbolic_execution:test
 

.github/workflows/artiweb.yml

@@ -13,7 +13,7 @@ jobs:
     steps:
       - name: 'Download artifact'
         id: da
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           script: |
             if (context.payload.workflow_run === undefined) {
@@ -57,7 +57,7 @@ jobs:
 
       - name: 'Read pr number'
         id: rpn
-        uses: actions/github-script@v6
+        uses: actions/github-script@v7
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
           script: |
@@ -67,7 +67,7 @@ jobs:
             core.setOutput("pr-number", issue_number_text === "" ? "" : Number(issue_number_text));
       - name: Find Comment
         if: ${{ steps.rpn.outputs.pr-number != '' }}
-        uses: peter-evans/find-comment@v2
+        uses: peter-evans/find-comment@v3
         id: fc
         with:
           issue-number: ${{ steps.rpn.outputs.pr-number }}
@@ -76,7 +76,7 @@ jobs:
 
       - name: Create or update comment
         if: ${{ steps.rpn.outputs.pr-number != '' }}
-        uses: peter-evans/create-or-update-comment@v2
+        uses: peter-evans/create-or-update-comment@v4
         with:
           comment-id: ${{ steps.fc.outputs.comment-id }}
           issue-number: ${{ steps.rpn.outputs.pr-number }}

.github/workflows/code_quality.yml

@@ -12,51 +12,51 @@ jobs:
   checkerFramework:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up JDK 21
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 21
           distribution: 'corretto'
           cache: 'gradle'
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: -DENABLE_NULLNESS=true compileTest
+        run: ./gradlew -DENABLE_NULLNESS=true compileTest
 
 
   qodana:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0
       - name: 'Qodana Scan'
-        uses: JetBrains/qodana-action@v2022.3.0
+        uses: JetBrains/qodana-action@v2024.1.5
 
-      - uses: github/codeql-action/upload-sarif@v2
+      - 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:
-      - uses: actions/checkout@v3
-      - uses: actions/setup-java@v3
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
         with:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: --continue spotlessCheck
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: SpotlessCheck
+        run: ./gradlew --continue spotlessCheck
 
   # checkstyle:
   #   runs-on: ubuntu-latest
   #   steps:
-  #     - uses: actions/checkout@v3
+  #     - uses: actions/checkout@v4
   #       with:
   #         fetch-depth: 0
   #     - run: scripts/tools/checkstyle/runIncrementalCheckstyle.sh --xml | tee report.xml
@@ -65,7 +65,7 @@ jobs:
   #         -v "CHECKSTYLE" "." ".*/report.xml$" "Checkstyle"     \
   #         -diff-to $(git merge-base HEAD origin/main) -pv false
 
-  #     - uses: github/codeql-action/upload-sarif@v2
+  #     - uses: github/codeql-action/upload-sarif@v3
   #       if: success() || failure()
   #       with:
   #         sarif_file: sarif-report.json
@@ -74,17 +74,16 @@ jobs:
   checkstyle_new:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
-      - uses: actions/setup-java@v3
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
         with:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: --continue checkstyleMainChanged
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Checkstyle
+        run: ./gradlew --continue checkstyleMainChanged
       - run: |
           npx violations-command-line -sarif sarif-report.json \
           -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle"
@@ -94,24 +93,24 @@ jobs:
 
       # $(git merge-base HEAD origin/main)
 
-      - uses: github/codeql-action/upload-sarif@v2
+      - 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@v3
-      - uses: actions/setup-java@v3
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
         with:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: --continue pmdMainChanged
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: PMD checks
+        run: ./gradlew --continue pmdMainChanged
 
       # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml
 
@@ -121,6 +120,6 @@ jobs:
 
       # -diff-from $(git merge-base HEAD origin/main)
       - name: Upload SARIF file
-        uses: github/codeql-action/upload-sarif@v2
+        uses: github/codeql-action/upload-sarif@v3
         with:
           sarif_file: pmd-report.json

.github/workflows/codeql.yml

@@ -27,17 +27,17 @@ jobs:
 
     steps:
     - name: Checkout repository
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Initialize CodeQL
-      uses: github/codeql-action/init@v2
+      uses: github/codeql-action/init@v3
       with:
         languages: ${{ matrix.language }}
 
     - name: Autobuild
-      uses: github/codeql-action/autobuild@v2
+      uses: github/codeql-action/autobuild@v3
 
     - name: Perform CodeQL Analysis
-      uses: github/codeql-action/analyze@v2
+      uses: github/codeql-action/analyze@v3
       with:
         category: "/language:${{matrix.language}}"

.github/workflows/gradle-publish.yml

@@ -12,26 +12,24 @@ jobs:
       packages: write
 
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     - name: Set up JDK 21
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         java-version: '21'
         distribution: 'corretto'
         cache: 'gradle'
         server-id: github # Value of the distributionManagement/repository/id field of the pom.xml
 
+    - name: Setup Gradle
+      uses: gradle/actions/setup-gradle@v3.3.2
     - name: Assemble with Gradle
-      uses: gradle/gradle-build-action@v2.4.2
-      with:
-        arguments: assemble
+      run: ./gradlew assemble
 
     # The USERNAME and TOKEN need to correspond to the credentials environment variables used in
     # the publishing section of your build.gradle
     - name: Publish to GitHub Packages
-      uses: gradle/gradle-build-action@v2.4.2
-      with:
-        arguments: publish
+      run: ./gradlew publish
       env:
         USERNAME: ${{ github.actor }}
         TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/javadoc.yml

@@ -8,27 +8,26 @@ jobs:
   doc:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - run: ls -ld
       - run: ls -lh 'gradle'
 
       - name: Set up JDK 21
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: '21'
           distribution: 'corretto'
           cache: 'gradle'
-
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: alldoc
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Build Documentation with Gradle
+        run: ./gradlew alldoc
 
       - name: Package
         run: tar cvfj javadoc.tar.bz2 build/docs/javadoc
 
       - name: Upload Javadoc
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: javadoc
           path: "javadoc.tar.bz2"

.github/workflows/nightlydeploy.yml

@@ -23,31 +23,30 @@ jobs:
       #     ignorePreReleases: true
       #     fetchReviewers: true
 
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up JDK 17
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 17
           distribution: 'temurin'
 
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: --parallel assemble
+        run: ./gradlew --parallel assemble
 
       - name: Delete previous nightly release
         continue-on-error: true
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          gh release delete nightly
-
+          gh release delete nightly --yes --cleanup-tag 
 
       - name: Create nightly release
         id: create_release
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |
+        run: |          
           gh release create --generate-notes --title "Nightly Release" \
              --prerelease \
              nightly key.ui/build/libs/key-*-exe.jar

.github/workflows/opttest.yml

@@ -16,24 +16,24 @@ jobs:
         tests: [":key.core.proof_references:test", ":key.core.symbolic_execution:test"]
     runs-on: ${{matrix.os}}
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up JDK ${{matrix.java}}
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: ${{matrix.java}}
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
-        with:
-          arguments: --continue ${{ matrix.tests }}
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Test with Gradle
+        run: ./gradlew --continue ${{ matrix.tests }}
 
       - name: Upload test results
-        uses: actions/upload-artifact@v3.1.1
+        uses: actions/upload-artifact@v4
         if: success() || failure()
         with:
-          name: test-results
+          name: test-results-${{ matrix.tests }}
           path: |
             **/build/test-results/*/*.xml
             **/build/reports/