Merge branch 'main' into weigl/pckgreworked

# Conflicts:
#	build.gradle
#	key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java

Author: wadoon

.github/workflows/code_quality.yml

@@ -20,7 +20,7 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - name: Build with Gradle
         run: ./gradlew -DENABLE_NULLNESS=true compileTest
 

.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@v4.1.0
+      uses: gradle/actions/setup-gradle@v4
     - 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@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - 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@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - 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@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - name: Test with Gradle
         run: ./gradlew --continue ${{ matrix.tests }}
 

.github/workflows/sonarqube.yml

@@ -13,29 +13,29 @@ jobs:
     name: Build and analyze
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0  # Shallow clones should be disabled for a better relevancy of analysis
       - name: Set up JDK 21
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 21
           distribution: 'zulu' 
       - name: Cache SonarCloud packages
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: ~/.sonar/cache
           key: ${{ runner.os }}-sonar
           restore-keys: ${{ runner.os }}-sonar
       - name: Cache Gradle packages
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: ~/.gradle/caches
           key: ${{ runner.os }}-gradle-${{ hashFiles('**/*.gradle') }}
           restore-keys: ${{ runner.os }}-gradle
 
       - name: Generate and submit dependency graph
-        uses: gradle/actions/dependency-submission@v3
+        uses: gradle/actions/dependency-submission@v4
         with:
             build-scan-publish: true
             build-scan-terms-of-use-url: "https://gradle.com/terms-of-service"

.github/workflows/tests.yml

@@ -38,7 +38,7 @@ jobs:
           cache: 'gradle'
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - name: Test with Gradle
         run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
@@ -53,7 +53,7 @@ jobs:
             !**/jacocoTestReport.xml
           
       - name: Upload coverage reports to Codecov
-        uses: codecov/codecov-action@v4
+        uses: codecov/codecov-action@v5
 
   integration-tests:
     env:
@@ -87,7 +87,7 @@ jobs:
         shell: bash
 
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - 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@v4.1.0
+          gradle/actions/setup-gradle@v4
       - 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@v4.1.0
+        uses: gradle/actions/setup-gradle@v4
       - name: "Running tests: ${{ matrix.test }}"
         run: ./gradlew --continue ${{ matrix.test }}
 

build.gradle

@@ -24,10 +24,9 @@ plugins {
     id "com.diffplug.spotless" version "6.25.0"
 
     // EISOP Checker Framework
+    id "org.checkerframework" version "0.6.48"
 
-    id "org.checkerframework" version "0.6.45"
-
-    id("org.sonarqube") version "5.0.0.4638"
+    id("org.sonarqube") version "6.0.1.5171"
 }
 
 sonar {
@@ -91,25 +90,26 @@ 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.12")
+        testImplementation("ch.qos.logback:logback-classic:1.5.15")
 
         //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:1.0.0")
         testCompileOnly("org.jspecify:jspecify:1.0.0")
-        def eisop_version = "3.42.0-eisop4"
+        def eisop_version = "3.42.0-eisop5"
         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-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker:$eisop_version"
 
-        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("ch.qos.logback:logback-classic:1.5.15")
+        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.4'
+        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.4'
         testImplementation project(':key.util')
 
-        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.3'
+        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.4'
     }
 
     tasks.withType(JavaCompile) {
@@ -352,10 +352,15 @@ subprojects {
             toggleOffOn()
 
             removeUnusedImports()
-            /* At the moment, we have to ensure that version 4.22 of the eclipse formatter is run, since newer versions
-             * of the formatter crash in SymbolicExecutionTreeBuilder (seems to be a but in the formatter)!
+
+            /* When new options are added in new versions of the Eclipse formatter, the easiest way is to export the new
+             * style file from the Eclipse GUI and then use the CodeStyleMerger tool in
+             * "$rootDir/scripts/tools/checkstyle/CodeStyleMerger.java" to merge the old and the new style files,
+             * i.e. "java CodeStyleMerger.java <oldStyleFile> <newStyleFile> keyCodeStyle.xml". The tool adds all
+             * entries with keys that were not present in the old file and optionally overwrites the old entries. The
+             * file is output with ordered keys, such that the file can easily be diffed using git.
              */
-            eclipse("4.22").configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
+            eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
             trimTrailingWhitespace()        // not sure how to set this in the xml file ...
             //googleJavaFormat().aosp().reflowLongStrings()
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java

@@ -6,7 +6,6 @@
 import java.util.Deque;
 import java.util.LinkedList;
 import java.util.List;
-import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.ldt.JavaDLTheory;
@@ -18,14 +17,12 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.JFunction;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
-import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.sort.Sort;
@@ -87,7 +84,7 @@ protected JFunction createResultFunction(Services services, Sort sort) {
      * @return The found result {@link Term} and the conditions.
      * @throws ProofInputException Occurred Exception.
      */
-    protected List<Triple<Term, Set<Term>, Node>> computeResultsAndConditions(Services services,
+    protected List<ResultsAndCondition> computeResultsAndConditions(Services services,
             Goal goal, ProofEnvironment sideProofEnvironment, Sequent sequentToProve,
             JFunction newPredicate) throws ProofInputException {
         return SymbolicExecutionSideProofUtil.computeResultsAndConditions(services, goal.proof(),
@@ -134,4 +131,5 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi
     public boolean isApplicableOnSubTerms() {
         return false;
     }
+
 }