Merge remote-tracking branch 'origin/main' into weigl/pckgreworked

# By Tobias Reinhold (27) and others
# Via GitHub (35) and others
* origin/main: (78 commits)
  spotless update
  removed default implementations for AbstractExternalSolverRuleApp around RULE field
  small formatting change
  Bump the gradle-deps group with 6 updates
  Bump JetBrains/qodana-action in the github-actions-deps group
  set version to 2.12.4-dev
  increase java version to 21
  added missing conversion rules from javaUnaryMinusFloat/Double to negFloat/Double
  add AbstractExternalSolverRuleApp to allow other external solvers to close goals
  fixes NullPointerException, when using compareTo with locations that dont have a URI or position
  Bump the github-actions-deps group with 2 updates
  Bump the gradle-deps group with 5 updates
  formatting
  Bump the github-actions-deps group with 2 updates
  Bump the gradle-deps group with 8 updates
  spotless
  generating ProofTree tooltips lazily, options to disable them completely
  fix for visual bug with overlapping/unreadable text in color settings
  Fox copyright year
  Bump the gradle-deps group with 6 updates
  ...

# Conflicts:
#	.github/workflows/code_quality.yml
#	build.gradle
#	key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
#	key.ui/src/main/java/de/uka/ilkd/key/ui/util/DoNothingCaret.java

.github/workflows/code_quality.yml

@@ -19,6 +19,8 @@ jobs:
           java-version: 21
           distribution: 'corretto'
           cache: 'gradle'
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: Build with Gradle
         uses: gradle/gradle-build-action@v3.3.2
         with:
@@ -34,6 +36,6 @@ jobs:
           java-version: '21'
           cache: 'gradle'
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
+        uses: gradle/gradle-build-action@v4.1.0
         with:
           arguments: --continue spotlessCheck

.github/workflows/gradle-publish.yml

@@ -22,7 +22,7 @@ jobs:
         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
+      uses: gradle/actions/setup-gradle@v4.1.0
     - name: Assemble with Gradle
       run: ./gradlew assemble
 

.github/workflows/javadoc.yml

@@ -19,7 +19,7 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: Build Documentation with Gradle
         run: ./gradlew alldoc
 

.github/workflows/nightlydeploy.yml

@@ -31,7 +31,7 @@ jobs:
           distribution: 'temurin'
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: Build with Gradle
         run: ./gradlew --parallel assemble
 

.github/workflows/opttest.yml

@@ -25,7 +25,7 @@ jobs:
           cache: 'gradle'
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: Test with Gradle
         run: ./gradlew --continue ${{ matrix.tests }}
 

.github/workflows/tests.yml

@@ -38,7 +38,7 @@ jobs:
           cache: 'gradle'
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: Test with Gradle
         run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
@@ -87,7 +87,7 @@ jobs:
         shell: bash
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: "Running tests: ${{ matrix.test }}"
         run: ./gradlew --continue ${{ matrix.test }}
 

.github/workflows/tests_winmac.yml

@@ -30,7 +30,7 @@ jobs:
 
       - name: Setup Gradle
         uses:
-          gradle/actions/setup-gradle@v3.3.2
+          gradle/actions/setup-gradle@v4.1.0
       - name: Test with Gradle
         run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
@@ -76,7 +76,7 @@ jobs:
         run: .github/dlsmt.sh
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v4.1.0
       - name: "Running tests: ${{ matrix.test }}"
         run: ./gradlew --continue ${{ matrix.test }}
 

build.gradle

@@ -25,7 +25,7 @@ plugins {
 
     // EISOP Checker Framework
 
-    id "org.checkerframework" version "0.6.41"
+    id "org.checkerframework" version "0.6.45"
 
     id("org.sonarqube") version "5.0.0.4638"
 }
@@ -52,10 +52,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"
@@ -74,13 +74,13 @@ subprojects {
     version = rootProject.version
 
     java {
-        sourceCompatibility = 17
-        targetCompatibility = 17
+        sourceCompatibility = 21
+        targetCompatibility = 21
     }
 
     repositories {
         mavenCentral()
-        maven { // cleary if needed?!
+        maven {
             url 'https://git.key-project.org/api/v4/projects/35/packages/maven'
         }
         maven { // remove if docking frames 1.1.3p2 on Maven Central
@@ -89,44 +89,42 @@ subprojects {
     }
 
     dependencies {
-        implementation("org.slf4j:slf4j-api:2.0.13")
-        implementation("org.slf4j:slf4j-api:2.0.13")
-        testImplementation("ch.qos.logback:logback-classic:1.5.6")
+        implementation("org.slf4j:slf4j-api:2.0.16")
+        implementation("org.slf4j:slf4j-api:2.0.16")
+        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'
 
-        compileOnly("org.jspecify:jspecify:0.3.0")
-        testCompileOnly("org.jspecify:jspecify:0.3.0")
-        def eisop_version = "3.42.0-eisop3"
+        compileOnly("org.jspecify:jspecify:1.0.0")
+        testCompileOnly("org.jspecify:jspecify:1.0.0")
+        def eisop_version = "3.42.0-eisop4"
         compileOnly "io.github.eisop:checker-qual:$eisop_version"
         compileOnly "io.github.eisop:checker-util:$eisop_version"
         testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker:$eisop_version"
 
-        testImplementation("ch.qos.logback:logback-classic:1.5.6")
-        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3'
-        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3'
+        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.10.3'
+        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
@@ -349,6 +347,8 @@ subprojects {
             targetExclude 'build/**'
 
             // allows us to use spotless:off / spotless:on to keep pre-formatted sections
+            // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on"
+            // that must be used instead.
             toggleOffOn()
 
             removeUnusedImports()

key.core/build.gradle

@@ -19,8 +19,8 @@ dependencies {
     javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0'
     antlr group: 'org.antlr', name: 'antlr', version: '3.5.3'   // use ANTLR version 3
 
-    antlr4 "org.antlr:antlr4:4.13.1"
-    api "org.antlr:antlr4-runtime:4.13.1"
+    antlr4 "org.antlr:antlr4:4.13.2"
+    api "org.antlr:antlr4-runtime:4.13.2"
     //implementation group: 'com.google.guava', name: 'guava', version: '28.1-jre'
 }
 

key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java

@@ -5,6 +5,7 @@
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
+import de.uka.ilkd.key.logic.util.EqualityUtils;
 
 import org.key_project.util.collection.ImmutableArray;
 
@@ -82,9 +83,29 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
         return true;
     }
 
+    /**
+     * Computes the hash code of {@code term} while ignoring irrelevant labels.
+     *
+     * @param term the term to compute the hash code for
+     * @return the hash code
+     */
     @Override
     public int hashCodeModThisProperty(Term term) {
-        throw new UnsupportedOperationException(
-            "Hashing of terms modulo irrelevant term labels not yet implemented!");
+        int hashcode = 5;
+        hashcode = hashcode * 17 + term.op().hashCode();
+        hashcode = hashcode * 17 + EqualityUtils
+                .hashCodeModPropertyOfIterable(IRRELEVANT_TERM_LABELS_PROPERTY, term.subs());
+        hashcode = hashcode * 17 + term.boundVars().hashCode();
+        hashcode = hashcode * 17 + term.javaBlock().hashCode();
+
+        final ImmutableArray<TermLabel> labels = term.getLabels();
+        for (int i = 0, sz = labels.size(); i < sz; i++) {
+            final TermLabel currentLabel = labels.get(i);
+            if (currentLabel.isProofRelevant()) {
+                hashcode += 7 * currentLabel.hashCode();
+            }
+        }
+
+        return hashcode;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java

@@ -8,11 +8,13 @@
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
+import de.uka.ilkd.key.logic.util.EqualityUtils;
 
 import org.key_project.util.EqualsModProofIrrelevancy;
 import org.key_project.util.EqualsModProofIrrelevancyUtil;
 import org.key_project.util.collection.ImmutableArray;
 
+
 /**
  * A property that can be used in
  * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} for terms.
@@ -104,7 +106,8 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
      */
     @Override
     public int hashCodeModThisProperty(Term term) {
-        int hashcode = Objects.hash(term.op(), hashCodeIterable(term.subs()),
+        int hashcode = Objects.hash(term.op(),
+            EqualityUtils.hashCodeModPropertyOfIterable(PROOF_IRRELEVANCY_PROPERTY, term.subs()),
             EqualsModProofIrrelevancyUtil.hashCodeIterable(term.boundVars()), term.javaBlock());
 
         // part from LabeledTermImpl
@@ -117,29 +120,4 @@ public int hashCodeModThisProperty(Term term) {
         }
         return hashcode;
     }
-
-    // -------------------------- Utility methods --------------------------------- //
-
-    /**
-     * Compute the hashcode mod proof irrelevancy of an iterable of terms using the elements'
-     * {@link EqualsModProperty} implementation.
-     *
-     * @param iter iterable of terms
-     * @return combined hashcode
-     */
-    public static int hashCodeIterable(Iterable<? extends Term> iter) {
-        // adapted from Arrays.hashCode
-        if (iter == null) {
-            return 0;
-        }
-
-        int result = 1;
-
-        for (Term element : iter) {
-            result = 31 * result + (element == null ? 0
-                    : element.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY));
-        }
-
-        return result;
-    }
 }