Post-Release 2.12.0: Backport bug fixes into main (#3242)

This PR merges the hotfixes and bugfixes into `main`.

.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/code_quality.yml

@@ -6,7 +6,7 @@ on:
   push:
     branches:
       - main
-      - 'releases/*'
+      - 'KeY-*'
 
 jobs:
   qodana:

.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/javadoc.yml

@@ -6,7 +6,6 @@ on:
 
 jobs:
   doc:
-    # later limit to master only!
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3

.github/workflows/tests.yml

@@ -5,7 +5,9 @@ on:
   push:
     branches: [ "main" ]
   pull_request:
-    branches: [ "main" ]
+    branches:
+      - "main"
+      - "KeY-*"
   merge_group:
 
 permissions:
@@ -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
@@ -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

@@ -13,7 +13,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-latest]
+        os: [macos-latest, ubuntu-latest, windows-latest]
         java: [11, 17]
     continue-on-error: true
     runs-on: ${{ matrix.os }}
@@ -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,7 +51,7 @@ jobs:
       fail-fast: false
       matrix:
         test: [testProveRules, testRunAllFunProofs, testRunAllInfProofs]
-        os: [ ubuntu-latest, windows-latest, macos-latest ]
+        os: [ macos-latest, ubuntu-latest, windows-latest ]
         java: [11,17]
     runs-on: ${{ matrix.os }}
     steps:
@@ -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
+

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.
 

build.gradle

@@ -49,13 +49,14 @@ static def getDate() {
 // The $BUILD_NUMBER is an environment variable set by Jenkins.
 def build = System.env.BUILD_NUMBER == null ? "" : "-${System.env.BUILD_NUMBER}"
 
-group = "org.key_project"
-version = "2.11.0$build"
+group = "org.key-project"
+version = "2.12.0$build"
 
 subprojects {
     apply plugin: "java"
     apply plugin: "java-library"
     apply plugin: "maven-publish"
+    apply plugin: "signing"       // GPG signing of artifacts, required by maven central
     apply plugin: "idea"
     apply plugin: "eclipse"
 
@@ -107,7 +108,7 @@ subprojects {
         //options.verbose()
         options.encoding = 'UTF-8'
         if (JavaVersion.current().isJava9Compatible()) {
-            //options.addBooleanOption('html5', true)
+            options.addBooleanOption('html5', true)
         }
     }
 
@@ -133,7 +134,6 @@ subprojects {
     }
 
 
-
     test {
         // Before we switched to JUnit 5, we used JUnit 4 with a customized discovery of test class.
         // This discovery called AutoSuite and searched in the compiled classes. AutoSuite was
@@ -180,28 +180,28 @@ subprojects {
     // The following two tasks can be used to execute main methods from the project
     // The main class is set via "gradle -DmainClass=... execute --args ..."
     // see https://stackoverflow.com/questions/21358466/gradle-to-execute-java-class-without-modifying-build-gradle
-    task execute(type:JavaExec) {
+    task execute(type: JavaExec) {
         description 'Execute main method from the project. Set main class via "gradle -DmainClass=... execute --args ..."'
         group "application"
         mainClass.set(System.getProperty('mainClass'))
         classpath = sourceSets.main.runtimeClasspath
     }
 
-    task executeInTests(type:JavaExec) {
+    task executeInTests(type: JavaExec) {
         description 'Execute main method from the project (tests loaded). Set main class via "gradle -DmainClass=... execute --args ..."'
         group "application"
         mainClass.set(System.getProperty('mainClass'))
         classpath = sourceSets.test.runtimeClasspath
     }
 
     // findbugs { findbugsTest.enabled = false; ignoreFailures = true }
-    pmd { 
+    pmd {
         pmdTest.enabled = false
-        ignoreFailures = true 
+        ignoreFailures = true
         toolVersion = "6.53.0"
         consoleOutput = false
         rulesMinimumPriority = 5
-        ruleSets = ["category/java/errorprone.xml",  "category/java/bestpractices.xml"]
+        ruleSets = ["category/java/errorprone.xml", "category/java/bestpractices.xml"]
     }
 
     task pmdMainChanged(type: Pmd) {
@@ -225,7 +225,7 @@ subprojects {
     checkstyle {
         toolVersion = "10.6.0"
         ignoreFailures = true
-        configFile file("$rootDir/gradle/key_checks.xml")        
+        configFile file("$rootDir/gradle/key_checks.xml")
         showViolations = false // disable console output
     }
 
@@ -249,9 +249,7 @@ subprojects {
                 outputLocation = file("build/reports/checkstyle/main_diff.xml")
             }
         }
-    } 
-
-
+    }
 
 
     // tasks.withType(FindBugs) {
@@ -260,13 +258,13 @@ subprojects {
     //         html.enabled = true
     //     }
     // }
-     tasks.withType(Pmd) {
-         reports {
-             xml.getRequired().set(true)
-             html.getRequired().set(true)
-         }
-     }
-    
+    tasks.withType(Pmd) {
+        reports {
+            xml.getRequired().set(true)
+            html.getRequired().set(true)
+        }
+    }
+
     task sourcesJar(type: Jar) {
         description = 'Create a jar file with the sources from this project'
         from sourceSets.main.allJava
@@ -281,7 +279,7 @@ subprojects {
 
     publishing {
         publications {
-            gpr(MavenPublication) {
+            mavenJava(MavenPublication) {
                 from components.java
                 artifact sourcesJar
                 artifact javadocJar
@@ -296,6 +294,7 @@ subprojects {
                             url = "http://www.gnu.org/licenses/old-licenses/gpl-2.0.html"
                         }
                     }
+
                     developers {
                         developer {
                             id = 'key'
@@ -313,10 +312,46 @@ subprojects {
         }
         repositories {
             maven {
+                /**
+                 * To be able to publish things on Maven Central, you need two things:
+                 *
+                 * (1) a JIRA account with permission on group-id `org.key-project`
+                 * (2) a keyserver-published GPG (w/o sub-keys)
+                 *
+                 * Your `$HOME/.gradle/gradle.properties` should like this:
+                 * ```
+                 * signing.keyId=YourKeyId
+                 * signing.password=YourPublicKeyPassword
+                 * ossrhUsername=your-jira-id
+                 * ossrhPassword=your-jira-password
+                 * ```
+                 *
+                 * You can test signing with `gradle sign`, and publish with `gradle publish`.
+                 * https://central.sonatype.org/publish/publish-guide/
+                 */
+                if (project.version.endsWith("-SNAPSHOT")) {
+                    name = "mavenSnapshot"
+                    url = "https://s01.oss.sonatype.org/content/repositories/snapshots/"
+                    credentials(PasswordCredentials) {
+                        username = project.properties.getOrDefault("ossrhUsername","")
+                        password = project.properties.getOrDefault("ossrhPassword","")
+                    }
+                } else {
+                    name = "mavenStaging"
+                    url = "https://s01.oss.sonatype.org/service/local/staging/deploy/maven2/"
+                    credentials(PasswordCredentials) {
+                        username = project.properties.getOrDefault("ossrhUsername","")
+                        password = project.properties.getOrDefault("ossrhPassword","")
+                    }
+                }
+            }
+
+            /*
+            maven { // deployment to git.key-project.org
                 name = "GitlabPackages"
                 url "https://git.key-project.org/api/v4/projects/35/packages/maven"
                 credentials(HttpHeaderCredentials) {
-                    if(System.getenv("TOKEN") != null) {
+                    if (System.getenv("TOKEN") != null) {
                         name = 'Private-Token'
                         value = System.getenv("TOKEN")
                     } else {
@@ -328,17 +363,23 @@ subprojects {
                     header(HttpHeaderAuthentication)
                 }
             }
+            */
         }
     }
 
+    signing {
+        useGpgCmd() // works better than the Java implementation, which requires PGP keyrings.
+        sign publishing.publications.mavenJava
+    }
+
     license {//configures the license file header
         header = file("$rootDir/gradle/header")
 
         mapping {
             //find styles here:
             // http://code.mycila.com/license-maven-plugin/#supported-comment-types
-            java="SLASHSTAR_STYLE" // DOUBLESLASH_STYLE
-            javascript="SLASHSTAR_STYLE"
+            java = "SLASHSTAR_STYLE" // DOUBLESLASH_STYLE
+            javascript = "SLASHSTAR_STYLE"
         }
         mapping("key", "SLASHSTAR_STYLE")
     }
@@ -437,7 +478,7 @@ task alldoc(type: Javadoc) {
         //stylesheetFile = new File( projectDir, 'src/javadoc/stylesheet.css' )
         windowTitle = 'KeY API Documentation'
         docTitle = "KeY JavaDoc ($project.version) -- ${getDate()}"
-        bottom = "Copyright &copy; 2003-2022 <a href=\"http://key-project.org\">The KeY-Project</a>."
+        bottom = "Copyright &copy; 2003-2023 <a href=\"http://key-project.org\">The KeY-Project</a>."
         use = true
         links += "https://docs.oracle.com/en/java/javase/11/docs/api/"
         links += "http://www.antlr2.org/javadoc/"
@@ -475,10 +516,10 @@ def getChangedFiles() {
     // Remove the status prefix
     def files = new TreeSet<String>()
     for (file in allFiles) {
-        if(file.length() > 1) {
+        if (file.length() > 1) {
             def a = file.substring(1).trim()
-            if(! a.isBlank() ) {
-                files.add(("$rootDir/"+a).toString())
+            if (!a.isBlank()) {
+                files.add(("$rootDir/" + a).toString())
             }
         }
     }

key.core/build.gradle

@@ -100,6 +100,7 @@ task generateSolverPropsList {
                 list.add(file.name)
             }
         })
+        list.sort()
         if (!file("$outputDir/$pack/solvers.txt").exists()) {
             String files = ''
             for (String propsFile : list) {
@@ -246,7 +247,4 @@ task generateRAPUnitTests(type: JavaExec) {
 }
 sourceSets.test.java.srcDirs("$buildDir/generated-src/rap/")
 
-
-// @AW: Delete? weigl: depends: If want that gradle check validates everything then not.
-// check.dependsOn << testProofRules << testRunAllProofs
-
+sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key, compileJavacc, generateGrammarSource)

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java

@@ -396,7 +396,7 @@ private List<recoder.java.CompilationUnit> recoderCompilationUnitsAsFiles(String
             if (ex.getCause() instanceof UnresolvedReferenceException) {
                 String extraMsg = "Consider using a classpath in your input file if this is a "
                     + "classtype that cannot be resolved (see "
-                    + "https://key-project.org/docs/user/Classpath for more details).";
+                    + "https://keyproject.github.io/key-docs/user/Classpath for more details).";
                 String msg = String.format("%s%n%s", ex.getCause().getMessage(), extraMsg);
                 reportError(msg, ex);
             } else {

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SMTCommand.java

@@ -85,7 +85,8 @@ private void runSMT(SMTCommandArguments args, SolverTypeCollection su, Goal goal
         for (SMTProblem problem : probList) {
             SMTSolverResult finalResult = problem.getFinalResult();
             if (finalResult.isValid() == ThreeValuedTruth.VALID) {
-                IBuiltInRuleApp app = RuleAppSMT.RULE.createApp(args.solver);
+                IBuiltInRuleApp app = SMTRuleApp.RULE.createApp(args.solver);
+                app = app.tryToInstantiate(problem.getGoal());
                 problem.getGoal().apply(app);
             }
             LOGGER.info("Finished run on goal " + goal.node().serialNr() + " in "