Merge branch 'main' into weigl/overop

* main: (109 commits) increase spotless version (and thus also eclipse formatter) to fix missing space in instanceof formatting Spotless and fix rebase Some additional minor fixes and spotlessApply Update `collect(Collectors.toList())` to `toList()` Introduction of record classes where it seems useful. Refactor: Introduce a pattern variable were possible. Translate large string concatenations into raw string literal (text blocks) update beanshell version in recoder's dependencies Switch to Java 17 for KeY-2.14.0 repair POM generation using afterEvaluate Adding license to KeY files Adding license to Java files add metadata for POM generation and update templates for license headers Bump ch.qos.logback:logback-classic from 1.4.8 to 1.4.11 Fix bug in icon selection update samplesIndex.txt Repair example index better default keyboard shortcuts, corrected docs URL, cleanup removing the SmansEtAl example from first touch change docking frames dependencies to maven central versions ...
KeYProject · Aug 27, 2023 · ccbe4c1 · ccbe4c1
2 parents 06f7acb + 6c808a3
commit ccbe4c1
Show file tree

Hide file tree

Showing 3,299 changed files with 15,024 additions and 13,088 deletions.
diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml
@@ -1,7 +1,7 @@
 blank_issues_enabled: false
 contact_links:
   - name: FAQ
-    url: https://key-project.org/docs/faq
+    url: https://keyproject.github.io/key-docs/faq
     about: Documentation 
   - name: KeY Discussions
     url: https://github.com/keyproject/key/discussions

diff --git a/.github/dlsmt.sh b/.github/dlsmt.sh
@@ -1,4 +1,4 @@
-#!/usr/bin/sh
+# No shebang!
 
 ## Weigl's little helper to download SMT-solvers. 
 # SPDX-License-Identifier: GPL-2.0-or-later

diff --git a/.github/workflows/artiweb.yml b/.github/workflows/artiweb.yml
@@ -83,6 +83,6 @@ jobs:
           body: |
             Thank you for your contribution.
             
-            The test artifacts are available on [Artiweb](https://keyproject.github.io/artiweb/${{steps.rpn.outputs.pr-number}}/).
-            The newest artifact is [here](https://keyproject.github.io/artiweb/${{steps.rpn.outputs.pr-number}}/${{steps.da.outputs.test-artifact-id}}/).
+            The test artifacts are available on [Artiweb](e8e3f762-a110-4e21-bc41-cacb5f3a3a50.ka.bw-cloud-instance.org/${{steps.rpn.outputs.pr-number}}/).
+            The newest artifact is [here](e8e3f762-a110-4e21-bc41-cacb5f3a3a50.ka.bw-cloud-instance.org/${{steps.rpn.outputs.pr-number}}/${{steps.da.outputs.test-artifact-id}}/).
           edit-mode: replace
diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml
@@ -6,7 +6,7 @@ on:
   push:
     branches:
       - main
-      - 'releases/*'
+      - 'KeY-*'
 
 jobs:
   qodana:
@@ -30,7 +30,7 @@ jobs:
       - uses: actions/setup-java@v3
         with:
           distribution: 'temurin'
-          java-version: '11'
+          java-version: '17'
       - name: Build with Gradle
         uses: gradle/[email protected]
         with:
@@ -61,7 +61,7 @@ jobs:
       - uses: actions/setup-java@v3
         with:
           distribution: 'temurin'
-          java-version: '11'
+          java-version: '17'
       - name: Build with Gradle
         uses: gradle/[email protected]
         with:
@@ -87,7 +87,7 @@ jobs:
       - uses: actions/setup-java@v3
         with:
           distribution: 'temurin'
-          java-version: '11'
+          java-version: '17'
       - name: Build with Gradle
         uses: gradle/[email protected]
         with:

diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
@@ -4,8 +4,9 @@ on:
   push:
     branches: [ "main" ]
   pull_request:
-    # The branches below must be a subset of the branches above
-    branches: [ "main" ]
+    branches:
+      - "main"
+      - "KeY-*"
   schedule:
     - cron: '21 21 * * 4'
   merge_group:

diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml
@@ -13,10 +13,10 @@ jobs:
 
     steps:
     - uses: actions/checkout@v3
-    - name: Set up JDK 11
+    - name: Set up JDK 17
       uses: actions/setup-java@v3
       with:
-        java-version: '11'
+        java-version: '17'
         distribution: 'temurin'
         server-id: github # Value of the distributionManagement/repository/id field of the pom.xml
 

diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml
@@ -6,17 +6,16 @@ on:
 
 jobs:
   doc:
-    # later limit to master only!
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
       - run: ls -ld
       - run: ls -lh 'gradle'
 
-      - name: Set up JDK 11
+      - name: Set up JDK 17
         uses: actions/setup-java@v3
         with:
-          java-version: '11'
+          java-version: '17'
           distribution: 'temurin'
 
       - name: Build with Gradle

diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml
@@ -12,7 +12,7 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-latest, windows-latest]
-        java: [11, 17]
+        java: [17]
         tests: [":key.core.proof_references:test", ":key.core.symbolic_execution:test"]
     runs-on: ${{matrix.os}}
     steps:

diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -5,7 +5,9 @@ on:
   push:
     branches: [ "main" ]
   pull_request:
-    branches: [ "main" ]
+    branches:
+      - "main"
+      - "KeY-*"
   merge_group:
 
 permissions:
@@ -21,7 +23,7 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-latest, windows-latest]
-        java: [11, 17]
+        java: [17]
     continue-on-error: true
     runs-on: ${{ matrix.os }}
     env:
@@ -44,7 +46,7 @@ jobs:
           name: pr-number
           path: pr/
       - uses: actions/checkout@v3
-      - name: Set up JDK 11
+      - name: Set up JDK 17
         uses: actions/setup-java@v3
         with:
           java-version: ${{ matrix.java }}
@@ -63,6 +65,8 @@ jobs:
           path: |
             **/build/test-results/*/*.xml
             **/build/reports/
+            !**/jacocoTestReport.xml
+            
 
       - name: Upload coverage reports to Codecov
         uses: codecov/codecov-action@v3
@@ -76,11 +80,11 @@ jobs:
       matrix:
         test: [testProveRules, testRunAllFunProofs, testRunAllInfProofs]
         os: [ubuntu-latest]
-        java: [11]
+        java: [17]
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v3
-      - name: Set up JDK 11
+      - name: Set up JDK 17
         uses: actions/setup-java@v3
         with:
           java-version: ${{ matrix.java }}
@@ -95,6 +99,8 @@ jobs:
 
       - name: Install SMT-Solvers
         run: .github/dlsmt.sh
+        shell: bash
+
 
       - name: "Running tests: ${{ matrix.test }}"
         uses: gradle/[email protected]

diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml
@@ -13,15 +13,15 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-latest]
-        java: [11, 17]
+        os: [macos-latest, ubuntu-latest, windows-latest]
+        java: [17]
     continue-on-error: true
     runs-on: ${{ matrix.os }}
     env:
       GH_TOKEN: ${{ github.token }}
     steps:
       - uses: actions/checkout@v3
-      - name: Set up JDK 11
+      - name: Set up JDK 17
         uses: actions/setup-java@v3
         with:
           java-version: ${{ matrix.java }}
@@ -36,13 +36,12 @@ jobs:
         uses: actions/[email protected]
         if: success() || failure()
         with:
-          name: test-results
+          name: test-results-${{ matrix.os }}
           path: |
             **/build/test-results/*/*.xml
             **/build/reports/
-
-      - name: Upload coverage reports to Codecov
-        uses: codecov/codecov-action@v3
+            !**/jacocoTestReport.xml
+            
 
   integration-tests:
     env:
@@ -52,12 +51,12 @@ jobs:
       fail-fast: false
       matrix:
         test: [testProveRules, testRunAllFunProofs, testRunAllInfProofs]
-        os: [ ubuntu-latest, windows-latest, macos-latest ]
-        java: [11,17]
+        os: [ macos-latest, ubuntu-latest, windows-latest ]
+        java: [17]
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v3
-      - name: Set up JDK 11
+      - name: Set up JDK 17
         uses: actions/setup-java@v3
         with:
           java-version: ${{ matrix.java }}
@@ -82,8 +81,10 @@ jobs:
         uses: actions/[email protected]
         if: success() || failure()        # run this step even if previous step failed
         with:
-          name: test-results
+          name: test-results-${{ matrix.os }}
           path: |
             **/build/test-results/*/*.xml
             key.core/build/reports/runallproofs/*
             **/build/reports/
+            !**/jacocoTestReport.xml
+
diff --git a/.github/workflows/update_symbex_oracles.yml b/.github/workflows/update_symbex_oracles.yml
@@ -17,10 +17,10 @@ jobs:
     continue-on-error: true
     steps:
       - uses: actions/checkout@v3
-      - name: Set up JDK 11
+      - name: Set up JDK 17
         uses: actions/setup-java@v3
         with:
-          java-version: '11'
+          java-version: '17'
           distribution: 'temurin'
 
       - name: Build with Gradle

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -5,7 +5,7 @@
 # Jenkins runs are triggered from somewhere else.
 #
 
-image: wadoon/key-test-docker:jdk11
+image: wadoon/key-test-docker:jdk17
 
 cache:
   policy: pull-push
@@ -47,7 +47,7 @@ compile:classes:
 compile:testClasses:
   dependencies:  ["compile:classes"]
   stage: secondary
-  image: wadoon/key-test-docker:jdk11
+  image: wadoon/key-test-docker:jdk17
   script:
     - javac -version
     - gradle --build-cache --parallel testClasses
@@ -61,7 +61,7 @@ compile:testClasses:
 sonarqube:
   dependencies:  ["compile:testClasses"]
   stage: ternary
-  image: wadoon/key-test-docker:jdk11
+  image: wadoon/key-test-docker:jdk17
   allow_failure: true
   script:
     - ./scripts/tools/sonarqube_hint.py
@@ -82,7 +82,7 @@ sonarqube:
 
 format:
   stage: primary
-  image: wadoon/key-test-docker:jdk11
+  image: wadoon/key-test-docker:jdk17
   allow_failure: true
   script:
     - gradle spotlessCheck

diff --git a/LICENSE.TXT b/LICENSE.TXT
@@ -27,8 +27,8 @@
        Sweden
 
 
-       WWW: http://key-project.org
-       e-mail: [email protected]	
+       WWW: https://www.key-project.org/
+       e-mail: [email protected]
 
        The KeY system is protected by the GNU General Public License.