Merge branch 'main' into ExternalSolverRuleApp

Author: BookWood7th

.github/workflows/code_quality.yml

@@ -32,7 +32,7 @@ jobs:
         with:
           fetch-depth: 0
       - name: 'Qodana Scan'
-        uses: JetBrains/qodana-action@v2024.2.3
+        uses: JetBrains/qodana-action@v2024.2.6
 
       - uses: github/codeql-action/upload-sarif@v3
         if: success() || failure()

build.gradle

@@ -24,7 +24,7 @@ plugins {
     id "com.diffplug.spotless" version "6.25.0"
 
     // EISOP Checker Framework
-    id "org.checkerframework" version "0.6.44"
+    id "org.checkerframework" version "0.6.45"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -40,10 +40,10 @@ static def getDate() {
 }
 
 // The $BUILD_NUMBER is an environment variable set by Jenkins.
-def build = System.env.BUILD_NUMBER == null ? "" : "-${System.env.BUILD_NUMBER}"
+def build = System.env.BUILD_NUMBER == null ? "-dev" : "-${System.env.BUILD_NUMBER}"
 
 group = "org.key-project"
-version = "2.13.0$build"
+version = "2.12.4$build"
 
 subprojects {
     apply plugin: "java"
@@ -62,8 +62,8 @@ subprojects {
     version = rootProject.version
 
     java {
-        sourceCompatibility = 17
-        targetCompatibility = 17
+        sourceCompatibility = 21
+        targetCompatibility = 21
     }
 
     repositories {
@@ -76,7 +76,7 @@ subprojects {
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.16")
         implementation("org.slf4j:slf4j-api:2.0.16")
-        testImplementation("ch.qos.logback:logback-classic:1.5.8")
+        testImplementation("ch.qos.logback:logback-classic:1.5.12")
 
         //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0'
         //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
@@ -89,29 +89,27 @@ subprojects {
         testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker:$eisop_version"
 
-        testImplementation("ch.qos.logback:logback-classic:1.5.8")
-        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.1'
-        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.1'
+        testImplementation("ch.qos.logback:logback-classic:1.5.12")
+        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.3'
+        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.3'
         testImplementation project(':key.util')
 
-        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.1'
+        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.3'
     }
 
     tasks.withType(JavaCompile) {
         // Setting UTF-8 as the java source encoding.
         options.encoding = "UTF-8"
-        // Setting the release to Java 17
-        options.release = 17
+        // Setting the release to Java 21
+        options.release = 21
     }
 
     tasks.withType(Javadoc) {
         failOnError = false
         options.addBooleanOption 'Xdoclint:none', true
         //options.verbose()
         options.encoding = 'UTF-8'
-        if (JavaVersion.current().isJava9Compatible()) {
-            options.addBooleanOption('html5', true)
-        }
+        options.addBooleanOption('html5', true)
     }
 
     tasks.withType(Test) {//Configure all tests

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key

@@ -8,6 +8,11 @@
 }
 
 \rules(programRules:Java, floatRules:assumeStrictfp) {
+    translateJavaUnaryMinusFloat {
+        \find(javaUnaryMinusFloat(f1))
+        \replacewith(negFloat(f1))
+        \heuristics(javaFloatSemantics)
+    };
 
     translateJavaAddFloat {
         \find(javaAddFloat(f1, f2))
@@ -33,6 +38,12 @@
         \heuristics(javaFloatSemantics)
     };
 
+    translateJavaUnaryMinusDouble {
+        \find(javaUnaryMinusDouble(d1))
+        \replacewith(negDouble(d1))
+        \heuristics(javaFloatSemantics)
+    };
+
     translateJavaAddDouble {
         \find(javaAddDouble(d1, d2))
         \replacewith(addDouble(d1, d2))

key.ui/build.gradle

@@ -23,7 +23,7 @@ dependencies {
     api 'com.miglayout:miglayout-swing:11.4.2'
 
     //logging implementation used by the slf4j
-    implementation 'ch.qos.logback:logback-classic:1.5.8'
+    implementation 'ch.qos.logback:logback-classic:1.5.12'
 
     api 'org.key-project:docking-frames-common:1.1.3p1'
     api 'org.key-project:docking-frames-core:1.1.3p1'

recoder/build.gradle

@@ -5,7 +5,7 @@ repositories {
     mavenCentral()
 }
 dependencies {
-    implementation 'org.ow2.asm:asm:9.7'
+    implementation 'org.ow2.asm:asm:9.7.1'
     implementation 'org.apache-extras.beanshell:bsh:2.0b6'
     implementation 'net.sf.retrotranslator:retrotranslator-runtime:1.2.9'
     implementation 'net.sf.retrotranslator:retrotranslator-transformer:1.2.9'