Merge branch 'main' into hein/bitwiseOperatorsTranslation

.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

.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

.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

.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:

.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:

.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
 

.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

.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:

.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]

.github/workflows/tests_winmac.yml

@@ -0,0 +1,90 @@
+name: Broad Release Tests
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron:  '0 5 * * 1' # every monday morning
+
+permissions:
+  checks: write
+
+jobs:
+  unit-tests:
+    strategy:
+      fail-fast: false
+      matrix:
+        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 17
+        uses: actions/setup-java@v3
+        with:
+          java-version: ${{ matrix.java }}
+          distribution: 'temurin'
+
+      - name: Build with Gradle
+        uses: gradle/[email protected]
+        with:
+          arguments: --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
+
+      - name: Upload test results
+        uses: actions/[email protected]
+        if: success() || failure()
+        with:
+          name: test-results-${{ matrix.os }}
+          path: |
+            **/build/test-results/*/*.xml
+            **/build/reports/
+            !**/jacocoTestReport.xml
+            
+
+  integration-tests:
+    env:
+      GH_TOKEN: ${{ github.token }}
+    continue-on-error: true
+    strategy:
+      fail-fast: false
+      matrix:
+        test: [testProveRules, testRunAllFunProofs, testRunAllInfProofs]
+        os: [ macos-latest, ubuntu-latest, windows-latest ]
+        java: [17]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up JDK 17
+        uses: actions/setup-java@v3
+        with:
+          java-version: ${{ matrix.java }}
+          distribution: 'temurin'
+
+      - name: Cache SMT-Solvers
+        id: smt-solvers
+        uses: actions/cache@v3
+        with:
+          path: smt-solvers
+          key: ${{ runner.os }}-smt-solvers
+
+      - name: Install SMT-Solvers
+        run: .github/dlsmt.sh
+
+      - name: "Running tests: ${{ matrix.test }}"
+        uses: gradle/[email protected]
+        with:
+          arguments: --continue ${{ matrix.test }}
+
+      - name: Upload test results
+        uses: actions/[email protected]
+        if: success() || failure()        # run this step even if previous step failed
+        with:
+          name: test-results-${{ matrix.os }}
+          path: |
+            **/build/test-results/*/*.xml
+            key.core/build/reports/runallproofs/*
+            **/build/reports/
+            !**/jacocoTestReport.xml
+

.github/workflows/update_symbex_oracles.yml

@@ -17,14 +17,14 @@ 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
-        uses: gradle/gradle-build-action@v2.3.3
+        uses: gradle/gradle-build-action@v2
         with:
           arguments: --continue -D UPDATE_TEST_ORACLE=true -D ORACLE_DIRECTORY=key.core.symbolic_execution/src/test/resources/testcase :key.core.symbolic_execution:test
 

.gitignore

@@ -64,3 +64,6 @@ key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/solvers.txt
 
 key/key.ui/examples/**/**.proof
 **/testresults/**
+
+scripts/tools/checkstyle/key_checks_incremental.xml
+checkstyle-diff.txt

.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

LICENSE.TXT

@@ -27,16 +27,14 @@
        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.
 
        The KeY system is free software; you can redistribute it 
-       and/or modify it under the terms of the GNU General 
-       Public License as published by the Free Software 
-       Foundation; either version 2 of the License, or (at your 
-       option) any later version. 
+       and/or modify it under the terms of the GNU General Public
+       License as published by the Free Software Foundation; version 2.
 
        This program is distributed in the hope that it will be 
        useful, but WITHOUT ANY WARRANTY; without