diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index 3d153e81f60..5410a014e96 100644 --- 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 index 5c4008dd815..904b5db74f9 100644 --- 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 index 3589f6623bb..d5dc9e44c78 100644 --- 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 index 649ffd635a5..4e047eafeb2 100644 --- 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 index bdc29f02f3d..250792c3a2c 100644 --- 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 index 0ac6a704ccb..bc34c820e96 100644 --- 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 index 1d99186c723..0d8cb6bc041 100644 --- 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 deleted file mode 100644 index 4561f81db10..00000000000 --- a/.project +++ /dev/null @@ -1,17 +0,0 @@ - - - key - Project key created by Buildship. - - - - - org.eclipse.buildship.core.gradleprojectbuilder - - - - - - org.eclipse.buildship.core.gradleprojectnature - - diff --git a/.settings/org.eclipse.buildship.core.prefs b/.settings/org.eclipse.buildship.core.prefs deleted file mode 100644 index e8895216fd3..00000000000 --- a/.settings/org.eclipse.buildship.core.prefs +++ /dev/null @@ -1,2 +0,0 @@ -connection.project.dir= -eclipse.preferences.version=1 diff --git a/build.gradle b/build.gradle index 9da6b06cc76..935addaa9a8 100644 --- 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 index bcfdb8916ed..d8435fc1005 100644 --- 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 index 9c4a9da821a..618a508badd 100644 --- 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 @@ - - - + + + diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java index f4544824321..71c67bd74e5 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java +++ b/key.core.symbolic_execution/src/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 heapContext = - HeapContext.getModHeaps(services, inst.transaction); + HeapContext.getModifiableHeaps(services, inst.transaction); Map atPreVars = UseOperationContractRule.computeAtPreVars(heapContext, services, inst); Map atPres = HeapContext.getAtPres(atPreVars, services); diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java index 606c82e328e..ef4d66447d4 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java +++ b/key.core.symbolic_execution/src/test/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/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java index 587c44c4811..e02a1979ce7 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java +++ b/key.core.symbolic_execution/src/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); } diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java index 39094494e49..2180b40ca21 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java @@ -51,74 +51,74 @@ public class TestThinBackwardSlicer extends AbstractSymbolicExecutionTestCase { private static final Logger LOGGER = LoggerFactory.getLogger(TestThinBackwardSlicer.class); /** - * Tests slicing on the example {@code blockContractAssignableLocationNotRequested}. + * Tests slicing on the example {@code blockContractModifiableLocationNotRequested}. * * @throws Exception Occurred Exception. */ @Test - public void testBlockContractAssignableLocationNotRequested() throws Exception { + public void testBlockContractModifiableLocationNotRequested() throws Exception { doSlicingTest( - "/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof", + "/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof", new ReturnSelector(122), true, 109, 14, 12); } /** - * Tests slicing on the example {@code blockContractAssignableRequestedLocation}. + * Tests slicing on the example {@code blockContractModifiableRequestedLocation}. * * @throws Exception Occurred Exception. */ @Test - public void testBlockContractAssignableRequestedLocation() throws Exception { + public void testBlockContractModifiableRequestedLocation() throws Exception { doSlicingTest( - "/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof", + "/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof", new ReturnSelector(111), true, 23); } /** - * Tests slicing on the example {@code blockContractAssignableEverything}. + * Tests slicing on the example {@code blockContractModifiableEverything}. * * @throws Exception Occurred Exception. */ @Test - public void testBlockContractAssignableEverything() throws Exception { + public void testBlockContractModifiableEverything() throws Exception { doSlicingTest( - "/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof", + "/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof", new ReturnSelector(97), true, 23); } /** - * Tests slicing on the example {@code methodContractAssignableLocationNotRequested}. + * Tests slicing on the example {@code methodContractModifiableLocationNotRequested}. * * @throws Exception Occurred Exception. */ @Test - public void testMethodContractAssignableLocationNotRequested() throws Exception { + public void testMethodContractModifiableLocationNotRequested() throws Exception { doSlicingTest( - "/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof", + "/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof", new ReturnSelector(29), true, 14, 12); } /** - * Tests slicing on the example {@code methodContractAssignableRequestedLocation}. + * Tests slicing on the example {@code methodContractModifiableRequestedLocation}. * * @throws Exception Occurred Exception. */ @Test - public void testMethodContractAssignableRequestedLocation() throws Exception { + public void testMethodContractModifiableRequestedLocation() throws Exception { doSlicingTest( - "/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof", + "/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof", new ReturnSelector(29), true, 23); } /** - * Tests slicing on the example {@code methodContractAssignableEverything}. + * Tests slicing on the example {@code methodContractModifiableEverything}. * * @throws Exception Occurred Exception. */ @Test - public void testMethodContractAssignableEverything() throws Exception { + public void testMethodContractModifiableEverything() throws Exception { doSlicingTest( - "/slicing/methodContractAssignableEverything/MethodContractAssignableExample.proof", + "/slicing/methodContractModifiableEverything/MethodContractModifiableExample.proof", new ReturnSelector(29), true, 23); } diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml similarity index 93% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml index a909f58e08d..a9489d5c9e3 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml @@ -1,6 +1,6 @@ - + @@ -27,8 +27,8 @@ mod allLocs \setMinus freshLocs(heap)termination diamond" pathCondition="true" p - - + + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.java b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.java similarity index 87% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.java rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.java index 7a5f1a3b1c4..738e953f0f4 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.java @@ -1,9 +1,9 @@ -public class BlockContractAssignableEverything { +public class BlockContractModifiableEverything { public static int x; - + public static int y; - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof similarity index 97% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof index a7d6685e106..4a684b3d7a9 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "BlockContractAssignableEverything[BlockContractAssignableEverything::main()].JML normal_behavior operation contract.0", + "name": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "BlockContractAssignableEverything[BlockContractAssignableEverything::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -149,7 +149,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "5") (term "1")) (rule "assignment_read_static_attribute" (formula "5") (term "1")) (builtin "One Step Simplification" (formula "5")) - (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableEverything_x_0")) + (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableEverything_x_0")) (rule "simplifySelectOfAnon" (formula "1")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml similarity index 95% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml index 0b9624d3278..c8172e0f445 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml @@ -1,6 +1,6 @@ - + @@ -9,7 +9,7 @@ pre measuredByEmpty post exc_0 = null mod {(null, - BlockContractAssignableLocationNotRequested::$y)}termination diamond" pathCondition="true" pathConditionChanged="false" preconditionComplied="false"> + BlockContractModifiableLocationNotRequested::$y)}termination diamond" pathCondition="true" pathConditionChanged="false" preconditionComplied="false"> @@ -25,7 +25,7 @@ mod {(null, - + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java similarity index 84% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java index f52e591322a..02f4f17b4b3 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java @@ -1,9 +1,9 @@ -public class BlockContractAssignableLocationNotRequested { +public class BlockContractModifiableLocationNotRequested { public static int x; - + public static int y; - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof similarity index 97% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof index c9dae84ca91..a72f618cb1d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "name": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -171,7 +171,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "5") (term "1")) (rule "assignment_read_static_attribute" (formula "5") (term "1")) (builtin "One Step Simplification" (formula "5")) - (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableLocationNotRequested_x_0")) + (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableLocationNotRequested_x_0")) (rule "simplifySelectOfAnon" (formula "1")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml similarity index 91% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml index ccd38bcd680..003fffcc5cd 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml @@ -1,6 +1,6 @@ - + @@ -8,7 +8,7 @@ +mod {(null, BlockContractModifiableRequestedLocation::$x)}termination diamond" pathCondition="true" pathConditionChanged="false" preconditionComplied="false"> @@ -24,8 +24,8 @@ mod {(null, BlockContractAssignableRequestedLocation::$x)}termination diamond" p - - + + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java similarity index 85% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java index 1cdba40e8be..9fd28452517 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java @@ -1,9 +1,9 @@ -public class BlockContractAssignableRequestedLocation { +public class BlockContractModifiableRequestedLocation { public static int x; - + public static int y; - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof similarity index 97% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof index 93c19bf9b10..1020268d01b 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation::main()].JML normal_behavior operation contract.0", + "name": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -177,7 +177,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "5") (term "1")) (rule "assignment_read_static_attribute" (formula "5") (term "1")) (builtin "One Step Simplification" (formula "5")) - (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableRequestedLocation_x_0")) + (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableRequestedLocation_x_0")) (rule "simplifySelectOfAnon" (formula "1")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinal.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptional.xml similarity index 62% rename from key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinal.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptional.xml index 4072f9325be..26286014a2f 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinal.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptional.xml @@ -1,16 +1,16 @@ - - - + + - +termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" selfTerm="self" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false"> + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalUnused.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalUnused.xml similarity index 65% rename from key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalUnused.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalUnused.xml index 07c84ff756e..32fe130b384 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalUnused.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalUnused.xml @@ -1,15 +1,15 @@ - - + - +termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" selfTerm="self" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false"> + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalVoid.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalVoid.xml similarity index 78% rename from key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalVoid.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalVoid.xml index 5ee15c6add9..7a55f8ba13a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalVoid.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalVoid.xml @@ -1,7 +1,7 @@ - - + - + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java index bd8210bfa21..0537d8ef083 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java @@ -1,7 +1,7 @@ public class InstanceContractTest { private int value; - + public int mainVoidMethod() { voidMethod(); return value; @@ -13,7 +13,7 @@ public int mainVoidMethod() { public void voidMethod() { value = 42; } - + public int mainNoArgs() { return noArgs(); } @@ -24,7 +24,7 @@ public int mainNoArgs() { public int noArgs() { return 42; } - + public int mainResult(int x) { return result(x); } @@ -36,9 +36,9 @@ public int mainResult(int x) { public int result(int x) { return x*x; } - - + + public int mainResultNotSpecified(int x) { return result(x); } @@ -50,35 +50,35 @@ public int mainResultNotSpecified(int x) { public int resultNotSpecified(int x) { return x*x; } - - public void mainExceptinalVoid(boolean x) throws Exception { - exceptinalVoid(x); + + public void mainExceptionalVoid(boolean x) throws Exception { + exceptionalVoid(x); } /*@ exceptional_behavior @ signals_only Exception; @ signals (Exception) true; @*/ - public void exceptinalVoid(boolean x) throws Exception { + public void exceptionalVoid(boolean x) throws Exception { throw new Exception(); } - - public void mainExceptinalUnused(boolean x) throws Exception { - exceptinal(x); + + public void mainExceptionalUnused(boolean x) throws Exception { + exceptional(x); } - - public boolean mainExceptinal(boolean x) throws Exception { - return exceptinal(x); + + public boolean mainExceptional(boolean x) throws Exception { + return exceptional(x); } /*@ exceptional_behavior @ signals_only Exception; @ signals (Exception) true; @*/ - public boolean exceptinal(boolean x) throws Exception { + public boolean exceptional(boolean x) throws Exception { throw new Exception(); } - + public void mainBooleanResultUnused(boolean x) { booleanResult(x); } @@ -89,7 +89,7 @@ public void mainBooleanResultUnused(boolean x) { public boolean booleanResult(boolean x) { return !x; } - + public void mainBooleanResultUnspecifiedUnused(boolean x) { booleanResultUnspecified(x); } @@ -100,20 +100,20 @@ public void mainBooleanResultUnspecifiedUnused(boolean x) { public boolean booleanResultUnspecified(boolean x) { return !x; } - + public void mainExceptionalConstructor() throws Exception { - new IntWrapper(); + new IntWrapper(); } - + public int mainConstructor() { IntWrapper w = new IntWrapper(42); return w.value; } - + public int mainOnObject(IntWrapper x) { return x.getValue(); } - + public static class IntWrapper { public int value; @@ -123,14 +123,14 @@ public static class IntWrapper { @*/ public IntWrapper() throws Exception { } - + /*@ normal_behavior @ ensures this.value == value; @*/ public IntWrapper(int value) { this.value = value; } - + /*@ normal_behavior @ ensures \result == value; @*/ diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinal.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptional.xml similarity index 57% rename from key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinal.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptional.xml index cc6ea0ee0a2..99a5c3f7766 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinal.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptional.xml @@ -1,13 +1,13 @@ - - - + + - +termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false"> + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalUnused.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalUnused.xml similarity index 60% rename from key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalUnused.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalUnused.xml index 03a4c684155..1d99c3547b9 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalUnused.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalUnused.xml @@ -1,12 +1,12 @@ - - + - +termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false"> + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalVoid.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalVoid.xml similarity index 74% rename from key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalVoid.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalVoid.xml index 6152d1b0f6b..2f58ae16b70 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalVoid.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalVoid.xml @@ -1,12 +1,12 @@ - - + - + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java index 2ee6a3c1835..489fcf778d2 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java @@ -1,7 +1,7 @@ public class StaticContractTest { private static int value; - + public static int mainVoidMethod() { voidMethod(); return value; @@ -13,7 +13,7 @@ public static int mainVoidMethod() { public static void voidMethod() { value = 42; } - + public static int mainNoArgs() { return noArgs(); } @@ -24,7 +24,7 @@ public static int mainNoArgs() { public static int noArgs() { return 42; } - + public static int mainResult(int x) { return result(x); } @@ -36,9 +36,9 @@ public static int mainResult(int x) { public static int result(int x) { return x*x; } - - + + public static int mainResultNotSpecified(int x) { return result(x); } @@ -50,35 +50,35 @@ public static int mainResultNotSpecified(int x) { public static int resultNotSpecified(int x) { return x*x; } - - public static void mainExceptinalVoid(boolean x) throws Exception { - exceptinalVoid(x); + + public static void mainExceptionalVoid(boolean x) throws Exception { + exceptionalVoid(x); } /*@ exceptional_behavior @ signals_only Exception; @ signals (Exception) true; @*/ - public static void exceptinalVoid(boolean x) throws Exception { + public static void exceptionalVoid(boolean x) throws Exception { throw new Exception(); } - - public static void mainExceptinalUnused(boolean x) throws Exception { - exceptinal(x); + + public static void mainExceptionalUnused(boolean x) throws Exception { + exceptional(x); } - - public static boolean mainExceptinal(boolean x) throws Exception { - return exceptinal(x); + + public static boolean mainExceptional(boolean x) throws Exception { + return exceptional(x); } /*@ exceptional_behavior @ signals_only Exception; @ signals (Exception) true; @*/ - public static boolean exceptinal(boolean x) throws Exception { + public static boolean exceptional(boolean x) throws Exception { throw new Exception(); } - + public static void mainBooleanResultUnused(boolean x) { booleanResult(x); } @@ -89,7 +89,7 @@ public static void mainBooleanResultUnused(boolean x) { public static boolean booleanResult(boolean x) { return !x; } - + public static void mainBooleanResultUnspecifiedUnused(boolean x) { booleanResultUnspecified(x); } @@ -100,20 +100,20 @@ public static void mainBooleanResultUnspecifiedUnused(boolean x) { public static boolean booleanResultUnspecified(boolean x) { return !x; } - + public static void mainExceptionalConstructor() throws Exception { - new IntWrapper(); + new IntWrapper(); } - + public static int mainConstructor() { IntWrapper w = new IntWrapper(42); return w.value; } - + public static int mainOnObject(IntWrapper x) { return x.getValue(); } - + public static class IntWrapper { public int value; @@ -123,14 +123,14 @@ public static class IntWrapper { @*/ public IntWrapper() throws Exception { } - + /*@ normal_behavior @ ensures this.value == value; @*/ public IntWrapper(int value) { this.value = value; } - + /*@ normal_behavior @ ensures \result == value; @*/ diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml similarity index 84% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml index 7057e7ebfce..c73153f380a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml @@ -1,9 +1,9 @@ - + - + diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.java b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.java similarity index 79% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.java rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.java index 2bb8e8ad5a6..b36e8eb69b7 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.java @@ -1,5 +1,5 @@ -public class ExceptinalAssignableNothingTest { +public class ExceptionalModifiableNothingTest { /*@ exceptional_behavior @ signals (NullPointerException) true; @ assignable \nothing; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof similarity index 99% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof index 26ade9e2935..5c5ed862ff5 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof @@ -42,8 +42,8 @@ \javaSource ""; \proofObligation { - "name": "ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest::main()].JML exceptional_behavior operation contract.0", - "contract": "ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest::main()].JML exceptional_behavior operation contract.0", + "name": "ExceptionalModifiableNothingTest[ExceptionalModifiableNothingTest::main()].JML exceptional_behavior operation contract.0", + "contract": "ExceptionalModifiableNothingTest[ExceptionalModifiableNothingTest::main()].JML exceptional_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof similarity index 99% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof index 2b4a8ce0717..05b2991d825 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof @@ -42,8 +42,8 @@ \javaSource ""; \proofObligation { - "name": "ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest::main()].JML exceptional_behavior operation contract.0", - "contract": "ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest::main()].JML exceptional_behavior operation contract.0", + "name": "ExceptionalModifiableNothingTest[ExceptionalModifiableNothingTest::main()].JML exceptional_behavior operation contract.0", + "contract": "ExceptionalModifiableNothingTest[ExceptionalModifiableNothingTest::main()].JML exceptional_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAssignableAndLoop/oracle/MagicProofNoOSS.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueModifiableAndLoop/oracle/MagicProofNoOSS.xml similarity index 100% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAssignableAndLoop/oracle/MagicProofNoOSS.xml rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueModifiableAndLoop/oracle/MagicProofNoOSS.xml diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAssignableAndLoop/test/ExampleInstance.java b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueModifiableAndLoop/test/ExampleInstance.java similarity index 100% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAssignableAndLoop/test/ExampleInstance.java rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueModifiableAndLoop/test/ExampleInstance.java diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAssignableAndLoop/test/MagicProofNoOSS.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueModifiableAndLoop/test/MagicProofNoOSS.proof similarity index 100% rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAssignableAndLoop/test/MagicProofNoOSS.proof rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueModifiableAndLoop/test/MagicProofNoOSS.proof diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.java b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.java similarity index 87% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.java rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.java index 7a5f1a3b1c4..738e953f0f4 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.java @@ -1,9 +1,9 @@ -public class BlockContractAssignableEverything { +public class BlockContractModifiableEverything { public static int x; - + public static int y; - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof similarity index 97% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof index a7d6685e106..4a684b3d7a9 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "BlockContractAssignableEverything[BlockContractAssignableEverything::main()].JML normal_behavior operation contract.0", + "name": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "BlockContractAssignableEverything[BlockContractAssignableEverything::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -149,7 +149,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "5") (term "1")) (rule "assignment_read_static_attribute" (formula "5") (term "1")) (builtin "One Step Simplification" (formula "5")) - (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableEverything_x_0")) + (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableEverything_x_0")) (rule "simplifySelectOfAnon" (formula "1")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.java b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.java similarity index 84% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.java rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.java index f52e591322a..02f4f17b4b3 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.java @@ -1,9 +1,9 @@ -public class BlockContractAssignableLocationNotRequested { +public class BlockContractModifiableLocationNotRequested { public static int x; - + public static int y; - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof similarity index 97% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof index c9dae84ca91..a72f618cb1d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "name": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -171,7 +171,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "5") (term "1")) (rule "assignment_read_static_attribute" (formula "5") (term "1")) (builtin "One Step Simplification" (formula "5")) - (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableLocationNotRequested_x_0")) + (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableLocationNotRequested_x_0")) (rule "simplifySelectOfAnon" (formula "1")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.java b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.java similarity index 85% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.java rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.java index 1cdba40e8be..9fd28452517 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.java @@ -1,9 +1,9 @@ -public class BlockContractAssignableRequestedLocation { +public class BlockContractModifiableRequestedLocation { public static int x; - + public static int y; - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof similarity index 97% rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof index 93c19bf9b10..1020268d01b 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation::main()].JML normal_behavior operation contract.0", + "name": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -177,7 +177,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "5") (term "1")) (rule "assignment_read_static_attribute" (formula "5") (term "1")) (builtin "One Step Simplification" (formula "5")) - (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableRequestedLocation_x_0")) + (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableRequestedLocation_x_0")) (rule "simplifySelectOfAnon" (formula "1")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableEverything/MethodContractAssignableExample.java b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableEverything/MethodContractModifiableExample.java similarity index 86% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableEverything/MethodContractAssignableExample.java rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableEverything/MethodContractModifiableExample.java index 6ad59bb292c..f7705a67021 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableEverything/MethodContractAssignableExample.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableEverything/MethodContractModifiableExample.java @@ -1,9 +1,9 @@ -public class MethodContractAssignableExample { +public class MethodContractModifiableExample { private static int x; - + private static int y; - + /*@ normal_behavior @ requires true; @ ensures true; @@ -15,7 +15,7 @@ public static int main() { magic(); return x; } - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableEverything/MethodContractAssignableExample.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableEverything/MethodContractModifiableExample.proof similarity index 95% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableEverything/MethodContractAssignableExample.proof rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableEverything/MethodContractModifiableExample.proof index eade3909e84..41295e2b1c2 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableEverything/MethodContractAssignableExample.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableEverything/MethodContractModifiableExample.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "MethodContractAssignableExample[MethodContractAssignableExample::main()].JML normal_behavior operation contract.0", + "name": "MethodContractModifiableExample[MethodContractModifiableExample::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "MethodContractAssignableExample[MethodContractAssignableExample::main()].JML normal_behavior operation contract.0", + "contract": "MethodContractModifiableExample[MethodContractModifiableExample::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -78,7 +78,7 @@ (builtin "One Step Simplification" (formula "3")) (rule "assignment_write_static_attribute" (formula "3") (term "1")) (builtin "One Step Simplification" (formula "3")) -(builtin "Use Operation Contract" (formula "3") (newnames "heapBefore_magic,exc_0,heapAfter_magic,anon_heap_magic") (contract "MethodContractAssignableExample[MethodContractAssignableExample::magic()].JML normal_behavior operation contract.0")) +(builtin "Use Operation Contract" (formula "3") (newnames "heapBefore_magic,exc_0,heapAfter_magic,anon_heap_magic") (contract "MethodContractModifiableExample[MethodContractModifiableExample::magic()].JML normal_behavior operation contract.0")) (branch "Post (magic)" (builtin "One Step Simplification" (formula "4")) (builtin "One Step Simplification" (formula "5")) @@ -89,7 +89,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "6") (term "1")) (rule "assignment_read_static_attribute" (formula "6") (term "1")) (builtin "One Step Simplification" (formula "6")) - (rule "pullOutSelect" (formula "6") (term "0,1,0") (inst "selectSK=MethodContractAssignableExample_x_0")) + (rule "pullOutSelect" (formula "6") (term "0,1,0") (inst "selectSK=MethodContractModifiableExample_x_0")) (rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "5")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.java b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.java similarity index 84% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.java rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.java index 2e90cebbb6f..c4bcb64b23b 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.java @@ -1,9 +1,9 @@ -public class MethodContractAssignableLocationNotRequested { +public class MethodContractModifiableLocationNotRequested { private static int x; - + private static int y; - + /*@ normal_behavior @ requires true; @ ensures true; @@ -15,7 +15,7 @@ public static int main() { magic(); return x; } - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof similarity index 94% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof index 824dad10a31..98b426854df 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "MethodContractAssignableLocationNotRequested[MethodContractAssignableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "name": "MethodContractModifiableLocationNotRequested[MethodContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "MethodContractAssignableLocationNotRequested[MethodContractAssignableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "contract": "MethodContractModifiableLocationNotRequested[MethodContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -78,7 +78,7 @@ (builtin "One Step Simplification" (formula "3")) (rule "assignment_write_static_attribute" (formula "3") (term "1")) (builtin "One Step Simplification" (formula "3")) -(builtin "Use Operation Contract" (formula "3") (newnames "heapBefore_magic,exc_0,heapAfter_magic,anon_heap_magic") (contract "MethodContractAssignableLocationNotRequested[MethodContractAssignableLocationNotRequested::magic()].JML normal_behavior operation contract.0")) +(builtin "Use Operation Contract" (formula "3") (newnames "heapBefore_magic,exc_0,heapAfter_magic,anon_heap_magic") (contract "MethodContractModifiableLocationNotRequested[MethodContractModifiableLocationNotRequested::magic()].JML normal_behavior operation contract.0")) (branch "Post (magic)" (builtin "One Step Simplification" (formula "4")) (builtin "One Step Simplification" (formula "5")) @@ -89,7 +89,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "6") (term "1")) (rule "assignment_read_static_attribute" (formula "6") (term "1")) (builtin "One Step Simplification" (formula "6")) - (rule "pullOutSelect" (formula "6") (term "0,1,0") (inst "selectSK=MethodContractAssignableLocationNotRequested_x_0")) + (rule "pullOutSelect" (formula "6") (term "0,1,0") (inst "selectSK=MethodContractModifiableLocationNotRequested_x_0")) (rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "5")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.java b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.java similarity index 84% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.java rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.java index b8e81778b82..9d4628e302c 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.java @@ -1,9 +1,9 @@ -public class MethodContractAssignableRequestedLocation { +public class MethodContractModifiableRequestedLocation { private static int x; - + private static int y; - + /*@ normal_behavior @ requires true; @ ensures true; @@ -15,7 +15,7 @@ public static int main() { magic(); return x; } - + /*@ normal_behavior @ requires true; @ ensures true; diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof similarity index 94% rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof rename to key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof index 6f408b3ada6..d8b66d819e4 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof @@ -42,9 +42,9 @@ \javaSource ""; \proofObligation { - "name": "MethodContractAssignableRequestedLocation[MethodContractAssignableRequestedLocation::main()].JML normal_behavior operation contract.0", + "name": "MethodContractModifiableRequestedLocation[MethodContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", "addSymbolicExecutionLabel": true, - "contract": "MethodContractAssignableRequestedLocation[MethodContractAssignableRequestedLocation::main()].JML normal_behavior operation contract.0", + "contract": "MethodContractModifiableRequestedLocation[MethodContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", } @@ -79,7 +79,7 @@ (builtin "One Step Simplification" (formula "3")) (rule "assignment_write_static_attribute" (formula "3") (term "1")) (builtin "One Step Simplification" (formula "3")) -(builtin "Use Operation Contract" (formula "3") (newnames "heapBefore_magic,exc_0,heapAfter_magic,anon_heap_magic") (contract "MethodContractAssignableRequestedLocation[MethodContractAssignableRequestedLocation::magic()].JML normal_behavior operation contract.0")) +(builtin "Use Operation Contract" (formula "3") (newnames "heapBefore_magic,exc_0,heapAfter_magic,anon_heap_magic") (contract "MethodContractModifiableRequestedLocation[MethodContractModifiableRequestedLocation::magic()].JML normal_behavior operation contract.0")) (branch "Post (magic)" (builtin "One Step Simplification" (formula "4")) (builtin "One Step Simplification" (formula "5")) @@ -90,7 +90,7 @@ (rule "activeUseStaticFieldReadAccess" (formula "6") (term "1")) (rule "assignment_read_static_attribute" (formula "6") (term "1")) (builtin "One Step Simplification" (formula "6")) - (rule "pullOutSelect" (formula "6") (term "0,1,0") (inst "selectSK=MethodContractAssignableRequestedLocation_x_0")) + (rule "pullOutSelect" (formula "6") (term "0,1,0") (inst "selectSK=MethodContractModifiableRequestedLocation_x_0")) (rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "5")) (builtin "One Step Simplification" (formula "1")) (rule "dismissNonSelectedField" (formula "1") (term "2,0")) diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java index 9ea2b64c61c..ed33123fa61 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java @@ -87,9 +87,9 @@ public Term getPreConTerm() { return services.getTermBuilder().ff(); } - public Term getAssignable() { + public Term getModifiable() { Contract c = getContract(); - return c.getAssignable(services.getTypeConverter().getHeapLDT().getHeap()); + return c.getModifiable(services.getTypeConverter().getHeapLDT().getHeap()); } public String getCode() { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index c652b73a373..3b0112a4f05 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java @@ -461,7 +461,7 @@ protected String getOracleAssertion(List oracleMethods) { oracleMethods.addAll(oracleGenerator.getOracleMethods()); LOGGER.debug("Modifier Set: {}", - oracleGenerator.getOracleLocationSet(info.getAssignable())); + oracleGenerator.getOracleLocationSet(info.getModifiable())); return "assertTrue(" + oracleCall + ");"; } diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index 03b7d3ce068..a8594d8bbf4 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -74,8 +74,22 @@ fragment Pfree: '_free'?; //suffix ACCESSIBLE: 'accessible' Pred -> pushMode(expr); ASSERT: 'assert' Pred -> pushMode(expr); ASSUME: 'assume' Pred -> pushMode(expr); -ASSIGNABLE: 'assignable' Pfree -> pushMode(expr); -ASSIGNS: 'assigns' Pred -> pushMode(expr); +/** + * The name 'assignable' is kept here for legacy reasons. + * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). + */ +ASSIGNABLE + : ('assignable' | 'assigns' | 'assigning' | + 'modifiable' | 'modifies' | 'modifying' | + 'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr); +/** + * The name 'assignable' is kept here for legacy reasons. + * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). + */ +LOOP_ASSIGNABLE + : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' | + 'loop_modifiable' | 'loop_modifies' | 'loop_modifying' | + 'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr); AXIOM: 'axiom' -> pushMode(expr); BREAKS: 'breaks' -> pushMode(expr); CAPTURES: 'captures' Pred -> pushMode(expr); @@ -87,7 +101,7 @@ DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr) DETERMINES: 'determines' -> pushMode(expr); DIVERGES: 'diverges' Pred -> pushMode(expr); //DURATION: 'duration' Pred -> pushMode(expr); -ENSURES: ('ensures' (Pfree|Pred) | 'post' Pred )-> pushMode(expr); +ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr); FOR_EXAMPLE: 'for_example' -> pushMode(expr); //FORALL: 'forall' -> pushMode(expr); //? HELPER: 'helper'; @@ -97,7 +111,7 @@ INITIALLY: 'initially' -> pushMode(expr); INSTANCE: 'instance'; INVARIANT: 'invariant' (Pfree|Pred) -> pushMode(expr); LOOP_CONTRACT: 'loop_contract'; -LOOP_INVARIANT: ('loop_invariant' (Pfree|Pred) | 'maintaining' Pred) -> pushMode(expr); +LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred) -> pushMode(expr); LOOP_DETERMINES: 'loop_determines'; // internal translation for 'determines' in loop invariants LOOP_SEPARATES: 'loop_separates'; //KeY extension, deprecated MAPS: 'maps' Pred -> pushMode(expr); @@ -105,8 +119,6 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr); MERGE_POINT: 'merge_point'; MERGE_PROC: 'merge_proc'; MERGE_PARAMS: 'merge_params' -> pushMode(expr); -MODIFIABLE: 'modifiable' Pred -> pushMode(expr); -MODIFIES: 'modifies' Pred -> pushMode(expr); MONITORED: 'monitored' -> pushMode(expr); MONITORS_FOR: 'monitors_for' -> pushMode(expr); //OLD: 'old' -> pushMode(expr); @@ -114,7 +126,7 @@ MONITORS_FOR: 'monitors_for' -> pushMode(expr); //PRE: 'pre' Pred -> pushMode(expr); READABLE: 'readable'; REPRESENTS: 'represents' Pred -> pushMode(expr); -REQUIRES: ('requires' (Pfree|Pred) | 'pre' Pred) -> pushMode(expr); +REQUIRES: ('requires'| 'pre') (Pfree|Pred) -> pushMode(expr); RETURN: 'return' -> pushMode(expr); RETURNS: 'returns' -> pushMode(expr); RESPECTS: 'respects' -> pushMode(expr); @@ -177,7 +189,7 @@ DEPENDS: 'depends'; // internal translation for 'accessible' on model fields /* JML and JML* keywords */ /*ACCESSIBLE: 'accessible'; -ASSIGNABLE: 'assignable'; +MODIFIABLE: 'modifiable'; BREAKS: 'breaks'; CONTINUES: 'continues'; DECREASES: 'decreases'; // internal translation for 'measured_by' diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 34819e845af..40f27ec6acc 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -87,7 +87,11 @@ accessible_clause (lhs=expression COLON)? rhs=storeRefUnion (MEASURED_BY mby=expression)? SEMI_TOPLEVEL; -assignable_clause: (ASSIGNABLE|MODIFIES|MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +/** + * The name 'assignable' is kept here for legacy reasons. + * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). + */ +assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ; //decreases_clause: DECREASES termexpression (COMMA termexpression)*; represents_clause @@ -174,10 +178,15 @@ loop_specification | determines_clause | loop_separates_clause | loop_determines_clause - | assignable_clause + | loop_assignable_clause | variant_function)*; loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL; +/** + * The name 'assignable' is kept here for legacy reasons. + * Note that KeY does only verify what can be modified (i.e., what is 'modifiable'). + */ +loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL; //loop_separates_clause: SEPARATES expression; //loop_determines_clause: DETERMINES expression; @@ -217,7 +226,7 @@ storeRefUnion: list = storeRefList; storeRefList: storeref (COMMA storeref)*; storeRefIntersect: storeRefList; storeref: (NOTHING | EVERYTHING | NOT_SPECIFIED | STRICTLY_NOTHING | storeRefExpr); -createLocset: (LOCSET | SINGLETON) LPAREN exprList RPAREN; +createLocset: (LOCSET | SINGLETON) LPAREN exprList? RPAREN; exprList: expression (COMMA expression)*; storeRefExpr: expression; predornot: (predicate |NOT_SPECIFIED | SAME); @@ -347,7 +356,7 @@ jmlprimary | VALUES #primaryValues | STRING_EQUAL LPAREN expression COMMA expression RPAREN #primaryStringEq | EMPTYSET #primaryEmptySet - | (LOCSET|STOREREF) LPAREN storeRefUnion RPAREN #primaryStoreRef + | (LOCSET|STOREREF) LPAREN storeRefUnion? RPAREN #primaryStoreRef | SINGLETON LPAREN expression RPAREN #primaryCreateLocsetSingleton | UNION LPAREN storeRefUnion RPAREN #primaryUnion | INTERSECT LPAREN storeRefIntersect RPAREN #primaryIntersect @@ -365,7 +374,7 @@ jmlprimary sequence : SEQEMPTY #sequenceEmpty | seqdefterm #sequenceIgnore1 - | (SEQSINGLETON | SEQ) LPAREN exprList RPAREN #sequenceCreate + | (SEQSINGLETON | SEQ) LPAREN exprList? RPAREN #sequenceCreate | SEQSUB LPAREN expression COMMA expression COMMA expression RPAREN #sequenceSub | SEQREVERSE LPAREN expression RPAREN #sequenceReverse | SEQREPLACE LPAREN expression COMMA expression COMMA expression RPAREN #sequenceReplace diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 19273162cd4..ab979bdf4fd 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -94,7 +94,7 @@ SKOLEMFORMULA : '\\skolemFormula'; TERMLABEL : '\\termlabel'; // used in contracts -MODIFIES : '\\modifies'; +MODIFIABLE : '\\modifiable'; // Keywords used in program variable declarations PROGRAMVARIABLES : '\\programVariables'; @@ -532,4 +532,4 @@ COMMENT_ANY_CHAR: . -> more; mode docComment; DOC_COMMENT_END: ('*/'|EOF) -> type(DOC_COMMENT), popMode; -DOC_COMMENT_ANY_CHAR: . -> more; \ No newline at end of file +DOC_COMMENT_ANY_CHAR: . -> more; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 6594f951ef8..d543bd0968e 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -823,7 +823,7 @@ one_contract : contractName = simple_ident LBRACE (prog_var_decls)? - fma=term MODIFIES modifiesClause=term + fma=term MODIFIABLE modifiableClause=term RBRACE SEMI ; diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiesSnippet.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiableSnippet.java similarity index 55% rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiesSnippet.java rename to key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiableSnippet.java index 7e33a02da20..e6a81c2d3fc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiesSnippet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiableSnippet.java @@ -11,17 +11,17 @@ * * @author christoph */ -class BasicModifiesSnippet extends ReplaceAndRegisterMethod implements FactoryMethod { +class BasicModifiableSnippet extends ReplaceAndRegisterMethod implements FactoryMethod { @Override public Term produce(BasicSnippetData d, ProofObligationVars poVars) throws UnsupportedOperationException { - if (d.get(BasicSnippetData.Key.MODIFIES) == null) { + if (d.get(BasicSnippetData.Key.MODIFIABLE) == null) { throw new UnsupportedOperationException( - "Tried to produce a " + "modifies-term for a contract without modifies."); + "Tried to produce a " + "modifiable-term for a contract without modifiable."); } - assert Term.class.equals(BasicSnippetData.Key.MODIFIES.getType()); - Term origMod = (Term) d.get(BasicSnippetData.Key.MODIFIES); - return replace(origMod, d.origVars, poVars.pre, d.tb); + assert Term.class.equals(BasicSnippetData.Key.MODIFIABLE.getType()); + Term origModifiable = (Term) d.get(BasicSnippetData.Key.MODIFIABLE); + return replace(origModifiable, d.origVars, poVars.pre, d.tb); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPOSnippetFactory.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPOSnippetFactory.java index e12139c34b4..bfe06db2b3f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPOSnippetFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPOSnippetFactory.java @@ -27,8 +27,8 @@ enum Snippet { // postcondition of the contract CONTRACT_POST(BasicPostconditionSnippet.class), - // modifies of the contract - CONTRACT_MOD(BasicModifiesSnippet.class), + // modifiable of the contract + CONTRACT_MODIFIABLE(BasicModifiableSnippet.class), // dependencies of the contract CONTRACT_DEP(BasicDependsSnippet.class), diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java index e3198b3d8cb..a42301f33a0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java @@ -90,7 +90,7 @@ enum Key { */ FREE_PRECONDITION(Term.class), POSTCONDITION(Term.class), LOOP_INVARIANT(LoopSpecification.class), LOOP_INVARIANT_TERM(Term.class), - MODIFIES(Term.class), DEPENDENS(Term.class), MEASURED_BY(Term.class), + MODIFIABLE(Term.class), DEPENDENS(Term.class), MEASURED_BY(Term.class), MODALITY(Modality.JavaModalityKind.class), INF_FLOW_SPECS(ImmutableList.class), /** * Self term of the transformed block contract @@ -125,7 +125,7 @@ public Class getType() { contractContents.put(Key.FOR_CLASS, contract.getKJT()); contractContents.put(Key.PRECONDITION, contract.getPre()); contractContents.put(Key.POSTCONDITION, contract.getPost()); - contractContents.put(Key.MODIFIES, contract.getMod()); + contractContents.put(Key.MODIFIABLE, contract.getModifiable()); contractContents.put(Key.MEASURED_BY, contract.getMby()); contractContents.put(Key.MODALITY, contract.getModalityKind()); @@ -145,22 +145,22 @@ public Class getType() { contractContents.put(Key.EXECUTION_CONTEXT, context); contractContents.put(Key.LOOP_INVARIANT, invariant); contractContents.put(Key.LOOP_INVARIANT_TERM, invariant.getInvariant(services)); - contractContents.put(Key.MODIFIES, invariant.getModifies()); + contractContents.put(Key.MODIFIABLE, invariant.getModifiable()); contractContents.put(Key.MODALITY, Modality.JavaModalityKind.BOX); contractContents.put(Key.INF_FLOW_SPECS, invariant.getInfFlowSpecs(services)); // add guard term to information flow specs (necessary for soundness) // and add the modified specs to the table ImmutableList infFlowSpecs = invariant.getInfFlowSpecs(services); - ImmutableList modifedSpecs = ImmutableSLList.nil(); + ImmutableList modifiedSpecs = ImmutableSLList.nil(); for (InfFlowSpec infFlowSpec : infFlowSpecs) { ImmutableList modifiedPreExps = infFlowSpec.preExpressions.append(guardTerm); ImmutableList modifiedPostExps = infFlowSpec.postExpressions.append(guardTerm); InfFlowSpec modifiedSpec = new InfFlowSpec(modifiedPreExps, modifiedPostExps, infFlowSpec.newObjects); - modifedSpecs = modifedSpecs.append(modifiedSpec); + modifiedSpecs = modifiedSpecs.append(modifiedSpec); } - contractContents.put(Key.INF_FLOW_SPECS, modifedSpecs); + contractContents.put(Key.INF_FLOW_SPECS, modifiedSpecs); final Term heap = tb.getBaseHeap(); final ImmutableSet localInVariables = @@ -187,7 +187,7 @@ public Class getType() { contractContents.put(Key.FOR_CLASS, contract.getKJT()); contractContents.put(Key.PRECONDITION, contract.getPre()); contractContents.put(Key.FREE_PRECONDITION, contract.getFreePre()); - contractContents.put(Key.MODIFIES, contract.getMod()); + contractContents.put(Key.MODIFIABLE, contract.getModifiable()); contractContents.put(Key.DEPENDENS, contract.getDep()); contractContents.put(Key.MEASURED_BY, contract.getMby()); contractContents.put(Key.MODALITY, contract.getModalityKind()); @@ -211,7 +211,7 @@ public Class getType() { contractContents.put(Key.BLOCK_SELF, contract.getInstantiationSelfTerm(services)); contractContents.put(Key.PRECONDITION, contract.getPre(services)); contractContents.put(Key.POSTCONDITION, contract.getPost(services)); - contractContents.put(Key.MODIFIES, contract.getMod(services)); + contractContents.put(Key.MODIFIABLE, contract.getModifiable(services)); contractContents.put(Key.MODALITY, contract.getModalityKind()); contractContents.put(Key.INF_FLOW_SPECS, contract.getInfFlowSpecs()); List