Merge branch 'main' into mulbrichPolymorphic

.github/workflows/code_quality.yml

@@ -20,7 +20,7 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v3.5.0
       - name: Build with Gradle
         run: ./gradlew -DENABLE_NULLNESS=true compileTest
 
@@ -32,7 +32,7 @@ jobs:
         with:
           fetch-depth: 0
       - name: 'Qodana Scan'
-        uses: JetBrains/[email protected].5
+        uses: JetBrains/[email protected].8
 
       - uses: github/codeql-action/upload-sarif@v3
         if: success() || failure()
@@ -49,7 +49,7 @@ jobs:
           java-version: '21'
           cache: 'gradle'
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v3.5.0
       - name: SpotlessCheck
         run: ./gradlew --continue spotlessCheck
 
@@ -81,7 +81,7 @@ jobs:
           java-version: '21'
           cache: 'gradle'
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v3.5.0
       - name: Checkstyle
         run: ./gradlew --continue checkstyleMainChanged
       - run: |
@@ -108,7 +108,7 @@ jobs:
           java-version: '21'
           cache: 'gradle'
       - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.3.2
+        uses: gradle/actions/setup-gradle@v3.5.0
       - name: PMD checks
         run: ./gradlew --continue pmdMainChanged
 

.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@v3.5.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@v3.5.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@v3.5.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@v3.5.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@v3.5.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@v3.5.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@v3.5.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@v3.5.0
       - name: "Running tests: ${{ matrix.test }}"
         run: ./gradlew --continue ${{ matrix.test }}
 

build.gradle

@@ -24,7 +24,7 @@ plugins {
     id "com.diffplug.spotless" version "6.25.0"
 
     // EISOP Checker Framework
-    id "org.checkerframework" version "0.6.39"
+    id "org.checkerframework" version "0.6.41"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -90,11 +90,11 @@ subprojects {
         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.2'
-        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2'
+        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3'
+        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3'
         testImplementation project(':key.util')
 
-        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2'
+        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.3'
     }
 
     tasks.withType(JavaCompile) {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -76,7 +76,7 @@
 import org.slf4j.LoggerFactory;
 
 import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
-import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
 
 /**
  * Provides utility methods for symbolic execution with KeY.
@@ -2686,7 +2686,7 @@ private static boolean checkReplaceTerm(Term toCheck, PosInOccurrence posInOccur
             Term replaceTerm) {
         Term termAtPio = followPosInOccurrence(posInOccurrence, toCheck);
         if (termAtPio != null) {
-            return termAtPio.equalsModProperty(replaceTerm, RENAMING_PROPERTY);
+            return termAtPio.equalsModProperty(replaceTerm, RENAMING_TERM_PROPERTY);
         } else {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java

@@ -24,7 +24,7 @@
 
 import org.key_project.util.collection.ImmutableList;
 
-import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
 
 
 /**
@@ -80,7 +80,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
         final Term selfComposedExec =
             f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION);
 
-        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
+        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java

@@ -25,7 +25,7 @@
 
 import org.key_project.util.collection.ImmutableList;
 
-import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
 
 public class StartAuxiliaryLoopComputationMacro extends AbstractProofMacro
         implements StartSideProofMacro {
@@ -77,7 +77,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
         final Term selfComposedExec =
             f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_LOOP_WITH_INV_RELATION);
 
-        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
+        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java

@@ -22,7 +22,7 @@
 
 import org.key_project.util.collection.ImmutableList;
 
-import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
 
 /**
  *
@@ -69,7 +69,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
         final Term selfComposedExec =
             f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_EXECUTION_WITH_PRE_RELATION);
 
-        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
+        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY);
     }
 
     @Override

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

@@ -45,25 +45,19 @@ public String getText() {
         return text;
     }
 
-
+    @Override
     public String toString() {
         return getText();
     }
 
-
-    /**
-     * comments can be ignored
-     */
-    public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
-        return true;
-    }
-
+    @Override
     public int hashCode() {
         int result = 17;
         result = 37 * result + getText().hashCode();
         return result;
     }
 
+    @Override
     public boolean equals(Object o) {
         if (o == this) {
             return true;

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

@@ -55,37 +55,28 @@ protected int getArrayPos(ImmutableArray<ProgramElement> arr, ProgramElement el)
         return -1;
     }
 
-
-    /**
-     * commented in interface SourceElement. Overwrites the default method implementation in
-     * ProgramElement by descending down to the children.
-     */
-    public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
-
-        if (se == this) {
+    @Override
+    public boolean equals(Object o) {
+        if (o == this) {
             return true;
-        } else if (se == null || this.getClass() != se.getClass()) {
+        }
+        if (o == null || o.getClass() != this.getClass()) {
             return false;
         }
 
-        final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) se;
+        final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) o;
         if (jnte.getChildCount() != getChildCount()) {
             return false;
         }
 
         for (int i = 0, cc = getChildCount(); i < cc; i++) {
-            if (!getChildAt(i).equalsModRenaming(jnte.getChildAt(i), nat)) {
+            if (!getChildAt(i).equals(jnte.getChildAt(i))) {
                 return false;
             }
         }
         return true;
     }
 
-    @Override
-    public boolean equals(Object o) {
-        return super.equals(o);
-    }
-
     @Override
     protected int computeHashCode() {
         int localHash = 17 * super.computeHashCode();

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

@@ -78,16 +78,6 @@ public Comment[] getComments() {
         return comments;
     }
 
-
-    /**
-     * commented in interface SourceElement. The default equals method compares two elements by
-     * testing if they have the same type and calling the default equals method.
-     */
-    @Override
-    public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
-        return (this.getClass() == se.getClass());
-    }
-
     protected int computeHashCode() {
         int result = 17 * this.getClass().hashCode();
         return result;
@@ -114,11 +104,10 @@ public boolean equals(Object o) {
         if (o == this) {
             return true;
         }
-        if (o == null || o.getClass() != this.getClass()) {
+        if (o == null) {
             return false;
         }
-
-        return equalsModRenaming((JavaProgramElement) o, NameAbstractionTableDisabled.INSTANCE);
+        return (this.getClass() == o.getClass());
     }
 
 

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

@@ -4,6 +4,8 @@
 package de.uka.ilkd.key.java;
 
 import de.uka.ilkd.key.java.visitor.Visitor;
+import de.uka.ilkd.key.logic.equality.EqualsModProperty;
+import de.uka.ilkd.key.logic.equality.Property;
 
 import org.key_project.logic.SyntaxElement;
 
@@ -13,7 +15,7 @@
  * to achieve an immutable structure
  */
 
-public interface SourceElement extends SyntaxElement {
+public interface SourceElement extends SyntaxElement, EqualsModProperty<SourceElement> {
 
 
     /**
@@ -93,8 +95,16 @@ public interface SourceElement extends SyntaxElement {
      * seen as {int decl_1; decl_1=0;} for the first one but {int decl_1; i=0;} for the second one.
      * These are not syntactical equal, therefore false is returned.
      */
-    boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat);
-
-
-
+    @Override
+    default <V> boolean equalsModProperty(Object o, Property<SourceElement> property, V... v) {
+        if (!(o instanceof SourceElement)) {
+            return false;
+        }
+        return property.equalsModThisProperty(this, (SourceElement) o, v);
+    }
+
+    @Override
+    default int hashCodeModProperty(Property<SourceElement> property) {
+        return property.hashCodeModThisProperty(this);
+    }
 }