Merge branch 'main' into mulbrichPolymorphic

KeYProject · Jun 21, 2024 · 566a3b8 · 566a3b8
2 parents 70d44e3 + c8b5d84
commit 566a3b8
Show file tree

Hide file tree

Showing 208 changed files with 2,295 additions and 2,006 deletions.
diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml
@@ -12,15 +12,15 @@ jobs:
   checkerFramework:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Set up JDK 21
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 21
           distribution: 'corretto'
           cache: 'gradle'
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v2.4.2
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: -DENABLE_NULLNESS=true compileTest
 
@@ -32,7 +32,7 @@ jobs:
         with:
           fetch-depth: 0
       - name: 'Qodana Scan'
-        uses: JetBrains/qodana-action@v2023.3.2
+        uses: JetBrains/qodana-action@v2024.1.5
 
       - uses: github/codeql-action/upload-sarif@v3
         if: success() || failure()
@@ -49,7 +49,7 @@ jobs:
           java-version: '21'
           cache: 'gradle'
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue spotlessCheck
 
@@ -82,7 +82,7 @@ jobs:
           cache: 'gradle'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue checkstyleMainChanged
       - run: |
@@ -109,7 +109,7 @@ jobs:
           java-version: '21'
           cache: 'gradle'
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue pmdMainChanged
 

diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml
@@ -22,14 +22,14 @@ jobs:
         server-id: github # Value of the distributionManagement/repository/id field of the pom.xml
 
     - name: Assemble with Gradle
-      uses: gradle/gradle-build-action@v3
+      uses: gradle/gradle-build-action@v3.3.2
       with:
         arguments: assemble
 
     # The USERNAME and TOKEN need to correspond to the credentials environment variables used in
     # the publishing section of your build.gradle
     - name: Publish to GitHub Packages
-      uses: gradle/gradle-build-action@v3
+      uses: gradle/gradle-build-action@v3.3.2
       with:
         arguments: publish
       env:

diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml
@@ -20,7 +20,7 @@ jobs:
           cache: 'gradle'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: alldoc
 

diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml
@@ -31,7 +31,7 @@ jobs:
           distribution: 'temurin'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --parallel assemble
 

diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml
@@ -25,7 +25,7 @@ jobs:
           cache: 'gradle'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue ${{ matrix.tests }}
 

diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -38,7 +38,7 @@ jobs:
           cache: 'gradle'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
@@ -88,7 +88,7 @@ jobs:
 
 
       - name: "Running tests: ${{ matrix.test }}"
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue ${{ matrix.test }}
 

diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml
@@ -29,7 +29,7 @@ jobs:
           cache: 'gradle'
 
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
@@ -75,7 +75,7 @@ jobs:
         run: .github/dlsmt.sh
 
       - name: "Running tests: ${{ matrix.test }}"
-        uses: gradle/gradle-build-action@v3
+        uses: gradle/gradle-build-action@v3.3.2
         with:
           arguments: --continue ${{ matrix.test }}
 

diff --git a/.project b/.project
diff --git a/.settings/org.eclipse.buildship.core.prefs b/.settings/org.eclipse.buildship.core.prefs
diff --git a/build.gradle b/build.gradle
@@ -24,7 +24,7 @@ plugins {
     id "com.diffplug.spotless" version "6.25.0"
 
     // EISOP Checker Framework
-    id "org.checkerframework" version "0.6.28"
+    id "org.checkerframework" version "0.6.39"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -75,15 +75,15 @@ subprojects {
 
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.13")
-        implementation("org.slf4j:slf4j-api:2.0.12")
-        testImplementation("ch.qos.logback:logback-classic:1.4.8")
+        implementation("org.slf4j:slf4j-api:2.0.13")
+        testImplementation("ch.qos.logback:logback-classic:1.5.6")
 
         //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-eisop2"
+        def eisop_version = "3.42.0-eisop3"
         compileOnly "io.github.eisop:checker-qual:$eisop_version"
         compileOnly "io.github.eisop:checker-util:$eisop_version"
         testCompileOnly "io.github.eisop:checker-qual:$eisop_version"

diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java
@@ -102,12 +102,12 @@ private void assignHandle(Attributes attributes) {
         categories2domains.put(p, domain);
     }
 
-    private void setAssignable(Attributes attributes) {
+    private void setModifiable(Attributes attributes) {
         assert tmpHandle == null;
         tmpHandle = attributes.getValue("handle");
     }
 
-    private void unsetAssignable() {
+    private void unsetModifiable() {
         assert tmpHandle != null;
         tmpHandle = null;
     }
@@ -214,7 +214,7 @@ public void startElement(String uri, String localName, String qName, Attributes
         // case "domainassignment":
         case "domains" -> startDomains();
         case "domain" -> putDomain(attributes);
-        case "assignable" -> setAssignable(attributes);
+        case "modifiable" -> setModifiable(attributes);
         case "field" -> putField(attributes);
         case "parameter" -> putParam(attributes);
         case "returnvalue" -> putReturn(attributes);
@@ -240,7 +240,7 @@ public void startElement(String uri, String localName, String qName, Attributes
     @Override
     public void endElement(String uri, String localName, String qName) {
         switch (localName) {
-        case "assignable" -> unsetAssignable();
+        case "modifiable" -> unsetModifiable();
         case "category" -> unsetCategory();
         case "domains" -> checkDomains();
         case "domainassignment" -> checkDomainAssignmentsWithFlows();

diff --git a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd
@@ -8,9 +8,9 @@
 <!ELEMENT flow EMPTY>
 <!ATTLIST flow from IDREF #REQUIRED to IDREF #REQUIRED>
 
-<!ELEMENT interfacespec (assignable)*>
-<!ELEMENT assignable (category | source | sink)>
-<!ATTLIST assignable handle ID #REQUIRED>
+<!ELEMENT interfacespec (modifiable)*>
+<!ELEMENT modifiable (category | source | sink)>
+<!ATTLIST modifiable handle ID #REQUIRED>
 <!ELEMENT category (category | source | sink)*>
 <!ATTLIST category name ID #REQUIRED>
 

diff --git a/...c/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java b/...c/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java
@@ -101,7 +101,7 @@ protected String lazyComputeName() throws ProofInputException {
             exceptionTerm = search.getExceptionEquality().sub(0);
             // Rename variables in contract to the current one
             List<LocationVariable> heapContext =
-                HeapContext.getModHeaps(services, inst.transaction);
+                HeapContext.getModifiableHeaps(services, inst.transaction);
             Map<LocationVariable, LocationVariable> atPreVars =
                 UseOperationContractRule.computeAtPreVars(heapContext, services, inst);
             Map<LocationVariable, Term> atPres = HeapContext.getAtPres(atPreVars, services);

diff --git a/...st/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/...st/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java
@@ -186,37 +186,37 @@ public void testUseOperationContractLightweightOperationContractTest() throws Ex
     }
 
     /**
-     * Tests example: /set/blockContractAssignableEverything
+     * Tests example: /set/blockContractModifiableEverything
      */
     @Test
-    public void testBlockContractAssignableEverything() throws Exception {
+    public void testBlockContractModifiableEverything() throws Exception {
         doSETTestAndDispose(testCaseDirectory,
-            "/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof",
-            "/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml",
+            "/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof",
+            "/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml",
             false, false, true, true, false, false, false, false, false, false, false, false,
             false);
     }
 
     /**
-     * Tests example: /set/blockContractAssignableLocationNotRequested
+     * Tests example: /set/blockContractModifiableLocationNotRequested
      */
     @Test
-    public void testBlockContractAssignableLocationNotRequested() throws Exception {
+    public void testBlockContractModifiableLocationNotRequested() throws Exception {
         doSETTestAndDispose(testCaseDirectory,
-            "/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof",
-            "/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml",
+            "/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof",
+            "/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml",
             false, false, true, true, false, false, false, false, false, false, false, false,
             false);
     }
 
     /**
-     * Tests example: /set/blockContractAssignableRequestedLocation
+     * Tests example: /set/blockContractModifiableRequestedLocation
      */
     @Test
-    public void testBlockContractAssignableRequestedLocation() throws Exception {
+    public void testBlockContractModifiableRequestedLocation() throws Exception {
         doSETTestAndDispose(testCaseDirectory,
-            "/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof",
-            "/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml",
+            "/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof",
+            "/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml",
             false, false, true, true, false, false, false, false, false, false, false, false,
             false);
     }

diff --git a/...c/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java b/...c/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java
@@ -89,10 +89,10 @@ public void testTruthValueLabelBelowUpdatesDifferentToApplicationTerm() throws E
     }
 
     /**
-     * Tests example: /set/truthValueExceptinalAssignableNothingTest
+     * Tests example: /set/truthValueExceptionalModifiableNothingTest
      */
     @Test
-    public void testExceptinalAssignableNothingTest_OSS() throws Exception {
+    public void testExceptionalModifiableNothingTest_OSS() throws Exception {
         // Create expected results
         ExpectedBranchResult goal374 =
             new ExpectedBranchResult(new ExpectedTruthValueResult("0.0", TruthValue.FALSE),
@@ -138,16 +138,16 @@ public void testExceptinalAssignableNothingTest_OSS() throws Exception {
             new ExpectedTruthValueEvaluationResult(goal374, goal407, goal444, goal475, goal476);
         // Perform test
         doTruthValueEvaluationTest(
-            "/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof",
-            "/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml",
+            "/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof",
+            "/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml",
             false, false, false, exceptionResult);
     }
 
     /**
-     * Tests example: /set/truthValueExceptinalAssignableNothingTest
+     * Tests example: /set/truthValueExceptionalModifiableNothingTest
      */
     @Test
-    public void testExceptinalAssignableNothingTest() throws Exception {
+    public void testExceptionalModifiableNothingTest() throws Exception {
         // Create expected results
         ExpectedBranchResult goal374 =
             new ExpectedBranchResult(new ExpectedTruthValueResult("0.0", TruthValue.FALSE),
@@ -193,8 +193,8 @@ public void testExceptinalAssignableNothingTest() throws Exception {
             new ExpectedTruthValueEvaluationResult(goal374, goal407, goal444, goal475, goal476);
         // Perform test
         doTruthValueEvaluationTest(
-            "/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof",
-            "/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml",
+            "/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof",
+            "/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml",
             false, false, false, exceptionResult);
     }
 
@@ -310,11 +310,11 @@ public void IGNORE_testAddingOfLabeledSubtree() throws Exception {
     }
 
     /**
-     * Tests example: /set/truthValueAssignableAndLoop
+     * Tests example: /set/truthValueModifiableAndLoop
      */
     @Test
     @Disabled
-    public void IGNORE_testAssignableAndLoop() throws Exception {
+    public void IGNORE_testModifiableAndLoop() throws Exception {
         // Create expected results
         ExpectedBranchResult goal430 =
             new ExpectedBranchResult(new ExpectedTruthValueResult("3.0", TruthValue.FALSE),
@@ -370,8 +370,8 @@ public void IGNORE_testAssignableAndLoop() throws Exception {
         ExpectedTruthValueEvaluationResult result5 =
             new ExpectedTruthValueEvaluationResult(goal1113, goal1134, goal1137);
         // Perform test
-        doTruthValueEvaluationTest("/set/truthValueAssignableAndLoop/test/MagicProofNoOSS.proof",
-            "/set/truthValueAssignableAndLoop/oracle/MagicProofNoOSS.xml", true, true, false,
+        doTruthValueEvaluationTest("/set/truthValueModifiableAndLoop/test/MagicProofNoOSS.proof",
+            "/set/truthValueModifiableAndLoop/oracle/MagicProofNoOSS.xml", true, true, false,
             resultExceptionBranch, resultInvInitial, resultPrecondition, resultLoopEnd, result5);
     }