Merge branch 'refs/heads/main' into weigl/pckgreworked

* refs/heads/main: (42 commits) EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm spotlessing ... making RuleCommand work if already fully instantiated RuleCommand can now deal with rules that have schema variables for logical variables. Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof obligation Code clean up (remove unused method) Fix loading of closed proofs (GUI threw error) Spotless fixes Fixed small typo in merge fixes. fix \locset() with empty args adding test cases for empty seq and locset. allow "\seq()" and "\locset()" in JML Bump the gradle-deps group with 6 updates Bump the github-actions-deps group with 4 updates Code formatting Adapted those qodana suggestions that are not false positives. Removed eclipse project file Also fixes for testcases Applied spotless ...
KeYProject · Jun 21, 2024 · 7200b6a · 7200b6a
2 parents 29e5cce + 4babbbe
commit 7200b6a
Show file tree

Hide file tree

Showing 211 changed files with 2,810 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:
@@ -78,15 +78,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);
     }