diff --git a/.github/dependabot.yml b/.github/dependabot.yml index a35c2aa153c..bcab3352493 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -5,7 +5,19 @@ version: 2 updates: - - package-ecosystem: "gradle" # See documentation for possible values - directory: "/" # Location of package manifests + - package-ecosystem: "gradle" + directory: "/" schedule: - interval: "weekly" + interval: "monthly" + groups: + gradle-deps: + patterns: + - "*" + - package-ecosystem: "github-actions" + directory: "/" + schedule: + interval: "monthly" + groups: + github-actions-deps: + patterns: + - "*" diff --git a/.github/workflows/update_symbex_oracles.yml b/.github/old_workflows/update_symbex_oracles.yml similarity index 91% rename from .github/workflows/update_symbex_oracles.yml rename to .github/old_workflows/update_symbex_oracles.yml index 3932b305972..405127c3c27 100644 --- a/.github/workflows/update_symbex_oracles.yml +++ b/.github/old_workflows/update_symbex_oracles.yml @@ -16,16 +16,16 @@ jobs: runs-on: ubuntu-latest continue-on-error: true 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 + uses: gradle/gradle-build-action@v3 with: arguments: --continue -D UPDATE_TEST_ORACLE=true -D ORACLE_DIRECTORY=key.core.symbolic_execution/src/test/resources/testcase :key.core.symbolic_execution:test diff --git a/.github/workflows/artiweb.yml b/.github/workflows/artiweb.yml index f4c6930722b..ca963363cf0 100644 --- a/.github/workflows/artiweb.yml +++ b/.github/workflows/artiweb.yml @@ -13,7 +13,7 @@ jobs: steps: - name: 'Download artifact' id: da - uses: actions/github-script@v6 + uses: actions/github-script@v7 with: script: | if (context.payload.workflow_run === undefined) { @@ -57,7 +57,7 @@ jobs: - name: 'Read pr number' id: rpn - uses: actions/github-script@v6 + uses: actions/github-script@v7 with: github-token: ${{ secrets.GITHUB_TOKEN }} script: | @@ -67,7 +67,7 @@ jobs: core.setOutput("pr-number", issue_number_text === "" ? "" : Number(issue_number_text)); - name: Find Comment if: ${{ steps.rpn.outputs.pr-number != '' }} - uses: peter-evans/find-comment@v2 + uses: peter-evans/find-comment@v3 id: fc with: issue-number: ${{ steps.rpn.outputs.pr-number }} @@ -76,7 +76,7 @@ jobs: - name: Create or update comment if: ${{ steps.rpn.outputs.pr-number != '' }} - uses: peter-evans/create-or-update-comment@v2 + uses: peter-evans/create-or-update-comment@v4 with: comment-id: ${{ steps.fc.outputs.comment-id }} issue-number: ${{ steps.rpn.outputs.pr-number }} diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index a3bd4d9a1b2..c6fd0d577c3 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -9,16 +9,32 @@ on: - 'KeY-*' jobs: + checkerFramework: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Set up JDK 21 + uses: actions/setup-java@v4 + with: + java-version: 21 + distribution: 'corretto' + cache: 'gradle' + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: Build with Gradle + run: ./gradlew -DENABLE_NULLNESS=true compileTest + + qodana: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: fetch-depth: 0 - name: 'Qodana Scan' - uses: JetBrains/qodana-action@v2022.3.0 + uses: JetBrains/qodana-action@v2024.1.8 - - uses: github/codeql-action/upload-sarif@v2 + - uses: github/codeql-action/upload-sarif@v3 if: success() || failure() with: sarif_file: ${{ runner.temp }}/qodana/results/qodana.sarif.json @@ -26,21 +42,21 @@ jobs: formatting: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 - - uses: actions/setup-java@v3 + - uses: actions/checkout@v4 + - uses: actions/setup-java@v4 with: distribution: 'corretto' java-version: '21' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue spotlessCheck + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: SpotlessCheck + run: ./gradlew --continue spotlessCheck # checkstyle: # runs-on: ubuntu-latest # steps: - # - uses: actions/checkout@v3 + # - uses: actions/checkout@v4 # with: # fetch-depth: 0 # - run: scripts/tools/checkstyle/runIncrementalCheckstyle.sh --xml | tee report.xml @@ -49,7 +65,7 @@ jobs: # -v "CHECKSTYLE" "." ".*/report.xml$" "Checkstyle" \ # -diff-to $(git merge-base HEAD origin/main) -pv false - # - uses: github/codeql-action/upload-sarif@v2 + # - uses: github/codeql-action/upload-sarif@v3 # if: success() || failure() # with: # sarif_file: sarif-report.json @@ -58,19 +74,18 @@ jobs: checkstyle_new: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 - - uses: actions/setup-java@v3 + - uses: actions/checkout@v4 + - uses: actions/setup-java@v4 with: distribution: 'corretto' java-version: '21' cache: 'gradle' - - - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue checkstyleMainChanged + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: Checkstyle + run: ./gradlew --continue checkstyleMainChanged - run: | - npx violations-command-line -sarif sarif-report.json -pv false \ + npx violations-command-line -sarif sarif-report.json \ -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle" #-diff-from $(git merge-base HEAD origin/main) @@ -78,7 +93,7 @@ jobs: # $(git merge-base HEAD origin/main) - - uses: github/codeql-action/upload-sarif@v2 + - uses: github/codeql-action/upload-sarif@v3 if: success() || failure() with: sarif_file: sarif-report.json @@ -86,25 +101,25 @@ jobs: pmd: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 - - uses: actions/setup-java@v3 + - uses: actions/checkout@v4 + - uses: actions/setup-java@v4 with: distribution: 'corretto' java-version: '21' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue pmdMainChanged + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: PMD checks + run: ./gradlew --continue pmdMainChanged # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml - run: | - npx violations-command-line -sarif pmd-report.json -pv false \ + npx violations-command-line -sarif pmd-report.json \ -v "PMD" "." ".*/build/reports/pmd/main_diff.xml$" "PMD" # -diff-from $(git merge-base HEAD origin/main) - name: Upload SARIF file - uses: github/codeql-action/upload-sarif@v2 + uses: github/codeql-action/upload-sarif@v3 with: sarif_file: pmd-report.json diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index ae93906d0fc..efdedd8caf2 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -27,17 +27,17 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Initialize CodeQL - uses: github/codeql-action/init@v2 + uses: github/codeql-action/init@v3 with: languages: ${{ matrix.language }} - name: Autobuild - uses: github/codeql-action/autobuild@v2 + uses: github/codeql-action/autobuild@v3 - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@v2 + uses: github/codeql-action/analyze@v3 with: category: "/language:${{matrix.language}}" diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml index 3a605988eb2..0a1ed3eb07e 100644 --- a/.github/workflows/gradle-publish.yml +++ b/.github/workflows/gradle-publish.yml @@ -12,26 +12,24 @@ jobs: packages: write 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' server-id: github # Value of the distributionManagement/repository/id field of the pom.xml + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 - name: Assemble with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: assemble + run: ./gradlew 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@v2.4.2 - with: - arguments: publish + run: ./gradlew publish env: USERNAME: ${{ github.actor }} TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index 9497dda5e71..8c3ed455250 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -8,27 +8,26 @@ jobs: doc: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - run: ls -ld - run: ls -lh 'gradle' - 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 - with: - arguments: alldoc + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: Build Documentation with Gradle + run: ./gradlew alldoc - name: Package run: tar cvfj javadoc.tar.bz2 build/docs/javadoc - name: Upload Javadoc - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: javadoc path: "javadoc.tar.bz2" diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 47b93efb6be..33b62b2c5c9 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -23,31 +23,30 @@ jobs: # ignorePreReleases: true # fetchReviewers: true - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up JDK 17 - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: 17 distribution: 'temurin' + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --parallel assemble + run: ./gradlew --parallel assemble - name: Delete previous nightly release continue-on-error: true env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | - gh release delete nightly - + gh release delete nightly --yes --cleanup-tag - name: Create nightly release id: create_release env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - run: | + run: | gh release create --generate-notes --title "Nightly Release" \ --prerelease \ nightly key.ui/build/libs/key-*-exe.jar diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index cfe001315de..75839cd76c5 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -16,24 +16,24 @@ jobs: tests: [":key.core.proof_references:test", ":key.core.symbolic_execution:test"] runs-on: ${{matrix.os}} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up JDK ${{matrix.java}} - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: ${{matrix.java}} distribution: 'corretto' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue ${{ matrix.tests }} + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: Test with Gradle + run: ./gradlew --continue ${{ matrix.tests }} - name: Upload test results - uses: actions/upload-artifact@v3.1.1 + uses: actions/upload-artifact@v4 if: success() || failure() with: - name: test-results + name: test-results-${{ matrix.tests }} path: | **/build/test-results/*/*.xml **/build/reports/ diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index bcab9f29453..e5f0041c442 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -29,48 +29,31 @@ jobs: env: GH_TOKEN: ${{ github.token }} steps: - - name: Save PR number - uses: actions/github-script@v6 - with: - script: | - const fs = require('fs'); - const util = require('util'); - fs.mkdirSync("./pr", { recursive: true }); - const payload = context.payload; - const number = (payload.issue || payload.pull_request || payload).number; - const text = number === undefined ? "" : String(number); - core.info("Pr number is " + number + ", writing \"" + text + "\""); - fs.writeFileSync("./pr/pr_number", text); - - uses: actions/upload-artifact@v3 - with: - name: pr-number - path: pr/ - - 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: ${{ matrix.java }} distribution: 'corretto' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 + - name: Test with Gradle + run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test - name: Upload test results - uses: actions/upload-artifact@v3.1.1 + uses: actions/upload-artifact@v4 if: success() || failure() with: - name: test-results + name: test-results-${{ matrix.os }} path: | **/build/test-results/*/*.xml **/build/reports/ !**/jacocoTestReport.xml - - + - name: Upload coverage reports to Codecov - uses: codecov/codecov-action@v3 + uses: codecov/codecov-action@v4 integration-tests: env: @@ -84,9 +67,9 @@ jobs: java: [21] runs-on: ${{ matrix.os }} 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: ${{ matrix.java }} distribution: 'corretto' @@ -94,7 +77,7 @@ jobs: - name: Cache SMT-Solvers id: smt-solvers - uses: actions/cache@v3 + uses: actions/cache@v4 with: path: smt-solvers key: ${{ runner.os }}-smt-solvers @@ -103,17 +86,16 @@ jobs: run: .github/dlsmt.sh shell: bash - + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 - name: "Running tests: ${{ matrix.test }}" - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue ${{ matrix.test }} + run: ./gradlew --continue ${{ matrix.test }} - name: Upload test results - uses: actions/upload-artifact@v3.1.1 + uses: actions/upload-artifact@v4 if: success() || failure() # run this step even if previous step failed with: - name: test-results + name: test-results-${{ matrix.test }} path: | **/build/test-results/*/*.xml key.core/build/reports/runallproofs/* diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml index 0b24edd9680..28335bd0998 100644 --- a/.github/workflows/tests_winmac.yml +++ b/.github/workflows/tests_winmac.yml @@ -20,21 +20,22 @@ jobs: env: GH_TOKEN: ${{ github.token }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up JDK ${{matrix.java}} - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: ${{ matrix.java }} distribution: 'corretto' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test + - name: Setup Gradle + uses: + gradle/actions/setup-gradle@v3.5.0 + - name: Test with Gradle + run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test - name: Upload test results - uses: actions/upload-artifact@v3.1.1 + uses: actions/upload-artifact@v4 if: success() || failure() with: name: test-results-${{ matrix.os }} @@ -56,9 +57,9 @@ jobs: java: [21] runs-on: ${{ matrix.os }} 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: ${{ matrix.java }} distribution: 'corretto' @@ -66,7 +67,7 @@ jobs: - name: Cache SMT-Solvers id: smt-solvers - uses: actions/cache@v3 + uses: actions/cache@v4 with: path: smt-solvers key: ${{ runner.os }}-smt-solvers @@ -74,13 +75,13 @@ jobs: - name: Install SMT-Solvers run: .github/dlsmt.sh + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.5.0 - name: "Running tests: ${{ matrix.test }}" - uses: gradle/gradle-build-action@v2.4.2 - with: - arguments: --continue ${{ matrix.test }} + run: ./gradlew --continue ${{ matrix.test }} - name: Upload test results - uses: actions/upload-artifact@v3.1.1 + uses: actions/upload-artifact@v4 if: success() || failure() # run this step even if previous step failed with: name: test-results-${{ matrix.os }} 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 f46b3c74247..61364ce00d4 100644 --- a/build.gradle +++ b/build.gradle @@ -22,6 +22,9 @@ plugins { // Code formatting id "com.diffplug.spotless" version "6.25.0" + + // EISOP Checker Framework + id "org.checkerframework" version "0.6.41" } // Configure this project for use inside IntelliJ: @@ -53,6 +56,7 @@ subprojects { apply plugin: "com.diffplug.spotless" apply plugin: "checkstyle" apply plugin: "pmd" + apply plugin: "org.checkerframework" group = rootProject.group version = rootProject.version @@ -70,18 +74,27 @@ subprojects { } dependencies { - implementation("org.slf4j:slf4j-api:2.0.12") - - testImplementation("ch.qos.logback:logback-classic:1.5.3") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2' + implementation("org.slf4j:slf4j-api:2.0.13") + 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-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" + checkerFramework "io.github.eisop:checker:$eisop_version" + + testImplementation("ch.qos.logback:logback-classic:1.5.6") + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3' testImplementation project(':key.util') - testCompileOnly 'junit:junit:4.13.2' - testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2' - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2' - - implementation("org.jspecify:jspecify:0.3.0") + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.3' } tasks.withType(JavaCompile) { @@ -348,6 +361,19 @@ subprojects { } } +// checkerFramework { +// checkers = [ +// "org.checkerframework.checker.nullness.NullnessChecker", +// ] +// extraJavacArgs = [ +// "-AonlyDefs=^org\\.key_project\\.util", +// "-Xmaxerrs", "10000", +// "-Astubs=$projectDir/src/main/checkerframework", +// "-Werror", +// "-Aversion", +// ] +// } + afterEvaluate { // required so project.description is non-null as set by sub build.gradle publishing { publications { diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index e411586a54a..48c0a02ca41 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists 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/blueprint_rifl.key b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key index 8a037c8ce28..23e944e4752 100644 --- a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key +++ b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key @@ -41,11 +41,11 @@ \javaSource "%%JAVA_SOURCE%%"; -\proofObligation "#Proof Obligation Settings -name=%%PO_NAME%% -contract=%%PO_NAME%% -class=de.uka.ilkd.key.informationflow.po.InfFlowContractPO -"; +\proofObligation { + "name": "%%PO_NAME%%", + "contract": "%%PO_NAME%%", + "class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO", + } \proofScript "macro 'infflow-autopilot';" 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/rule/label/FormulaTermLabelRefactoring.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java index 8773f536ec1..f55f6111dcc 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java @@ -384,7 +384,7 @@ public static boolean containsSequentFormulasToRefactor(TermLabelState state) { @SuppressWarnings("unchecked") Set sfSet = (Set) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED); - return !CollectionUtil.isEmpty(sfSet); + return sfSet != null && !sfSet.isEmpty(); } /** diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java index 87deb6675f6..293a231f50f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java @@ -175,10 +175,10 @@ protected void collectRemembranceVariables(Term term, if (SymbolicExecutionUtil.isHeap(eu.lhs(), getServices().getTypeConverter().getHeapLDT())) { remembranceHeaps.put((LocationVariable) term.sub(0).op(), - getServices().getTermBuilder().var(eu.lhs())); + getServices().getTermBuilder().varOfUpdateableOp(eu.lhs())); } else { remembranceLocalVariables.put((LocationVariable) term.sub(0).op(), - getServices().getTermBuilder().var(eu.lhs())); + getServices().getTermBuilder().varOfUpdateableOp(eu.lhs())); } } else { assert false : "Unsupported update term with operator '" + term.op() + "'."; 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/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java index a8e23732cb9..726d64d25fa 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java @@ -26,6 +26,7 @@ import de.uka.ilkd.key.pp.PrettyPrinter; import de.uka.ilkd.key.proof.init.AbstractOperationPO; import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.speclang.jml.translation.Context; import de.uka.ilkd.key.speclang.njml.JmlIO; @@ -156,8 +157,8 @@ protected ImmutableList buildOperationBlocks( * {@inheritDoc} */ @Override - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { return tb.tt(); } @@ -165,8 +166,8 @@ protected Term generateMbyAtPreDef(ProgramVariable selfVar, * {@inheritDoc} */ @Override - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { if (precondition != null && !precondition.isEmpty()) { var context = Context.inMethod(getProgramMethod(), services.getTermBuilder()); @@ -183,9 +184,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, * {@inheritDoc} */ @Override - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { return tb.tt(); } @@ -195,7 +196,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, */ @Override protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { return tb.tt(); } @@ -263,14 +265,17 @@ public String getPrecondition() { /** * {@inheritDoc} + * + * @return */ @Override - public void fillSaveProperties(Properties properties) { - super.fillSaveProperties(properties); - properties.setProperty("method", getProgramMethodSignature(getProgramMethod(), true)); + public Configuration createLoaderConfig() { + var c = super.createLoaderConfig(); + c.set("method", getProgramMethodSignature(getProgramMethod(), true)); if (getPrecondition() != null && !getPrecondition().isEmpty()) { - properties.setProperty("precondition", getPrecondition()); + c.set("precondition", getPrecondition()); } + return c; } /** @@ -294,34 +299,19 @@ public static String getProgramMethodSignature(IProgramMethod pm, boolean includ return x.result(); } - /** - * Instantiates a new proof obligation with the given settings. - * - * @param initConfig The already load {@link InitConfig}. - * @param properties The settings of the proof obligation to instantiate. - * @return The instantiated proof obligation. - * @throws IOException Occurred Exception. - */ - public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) - throws IOException { - return new LoadedPOContainer(new ProgramMethodPO(initConfig, getName(properties), - getProgramMethod(initConfig, properties), getPrecondition(properties), - isAddUninterpretedPredicate(properties), isAddSymbolicExecutionLabel(properties))); - } - /** * Searches the {@link IProgramMethod} defined by the given {@link Properties}. * - * @param initConfig The already load {@link InitConfig}. + * @param initConfig The already loaded {@link InitConfig}. * @param properties The settings of the proof obligation to instantiate. * @return The found {@link IProgramMethod}. * @throws IOException Occurred Exception if it was not possible to find the * {@link IProgramMethod}. */ - public static IProgramMethod getProgramMethod(InitConfig initConfig, Properties properties) + public static IProgramMethod getProgramMethod(InitConfig initConfig, Configuration properties) throws IOException { // Get container class and method signature - String value = properties.getProperty("method"); + String value = properties.getString("method"); if (value == null) { throw new IOException("Property \"method\" is not defined."); } @@ -380,8 +370,8 @@ public static IProgramMethod getProgramMethod(InitConfig initConfig, Properties * @param properties The proof obligation settings to read from. * @return The precondition or {@code null} if not available. */ - public static String getPrecondition(Properties properties) { - return properties.getProperty("precondition"); + public static String getPrecondition(Configuration properties) { + return properties.getString("precondition"); } @Override diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPOLoader.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPOLoader.java new file mode 100644 index 00000000000..78f56ccec67 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPOLoader.java @@ -0,0 +1,44 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.symbolic_execution.po; + +import java.io.IOException; + +import de.uka.ilkd.key.proof.init.IPersistablePO; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.init.loader.ProofObligationLoader; +import de.uka.ilkd.key.settings.Configuration; + +import org.jspecify.annotations.NullMarked; + +import static de.uka.ilkd.key.proof.init.AbstractPO.getName; +import static de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO.*; + +@NullMarked +public class ProgramMethodPOLoader implements ProofObligationLoader { + /** + * Instantiates a new proof obligation with the given settings. + * + * @param initConfig The already load {@link InitConfig}. + * @param properties The settings of the proof obligation to instantiate. + * @return The instantiated proof obligation. + */ + @Override + public IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, + Configuration properties) + throws IOException { + return new IPersistablePO.LoadedPOContainer(new ProgramMethodPO(initConfig, + getName(properties), + ProgramMethodPO.getProgramMethod(initConfig, properties), getPrecondition(properties), + isAddUninterpretedPredicate(properties), isAddSymbolicExecutionLabel(properties))); + } + + @Override + public boolean handles(String identifier) { + return ProgramMethodPOLoader.class.getSimpleName().equals(identifier) + || ProgramMethodPOLoader.class.getName().equals(identifier) + || ProgramMethodPO.class.getSimpleName().equals(identifier) + || ProgramMethodPO.class.getName().equals(identifier); + } +} diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java index 1405ff15f6c..46547b4935b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java @@ -22,6 +22,7 @@ import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.settings.Configuration; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -82,6 +83,10 @@ */ //spotless:on public class ProgramMethodSubsetPO extends ProgramMethodPO { + public static final String START_LINE = "startLine"; + public static final String START_COLUMN = "startColumn"; + public static final String END_LINE = "endLine"; + public static final String END_COLUMN = "endColumn"; /** * Contains all undeclared variables used in the method part to execute. */ @@ -219,10 +224,10 @@ protected boolean endsWithReturn(Statement[] statements) { * {@inheritDoc} */ @Override - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { - ImmutableList paramVarsList = + ImmutableList paramVarsList = convert(undeclaredVariableCollector.result()); return super.getPre(modHeaps, selfVar, paramVarsList, atPreVars, services); } @@ -231,10 +236,10 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, * {@inheritDoc} */ @Override - protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, - ImmutableList paramVars, List heaps, + protected Term buildFreePre(LocationVariable selfVar, KeYJavaType selfKJT, + ImmutableList paramVars, List heaps, Services proofServices) { - ImmutableList paramVarsList = + ImmutableList paramVarsList = convert(undeclaredVariableCollector.result()); return super.buildFreePre(selfVar, selfKJT, paramVarsList, heaps, proofServices); } @@ -243,10 +248,10 @@ protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, * {@inheritDoc} */ @Override - protected Term ensureUninterpretedPredicateExists(ImmutableList paramVars, - ImmutableList formalParamVars, ProgramVariable exceptionVar, + protected Term ensureUninterpretedPredicateExists(ImmutableList paramVars, + ImmutableList formalParamVars, LocationVariable exceptionVar, String name, Services proofServices) { - ImmutableList paramVarsList = + ImmutableList paramVarsList = convert(undeclaredVariableCollector.result()); return super.ensureUninterpretedPredicateExists(paramVarsList, formalParamVars, exceptionVar, name, proofServices); @@ -258,8 +263,8 @@ protected Term ensureUninterpretedPredicateExists(ImmutableList * @param c The {@link Collection} to convert. * @return The created {@link ImmutableList}. */ - protected static ImmutableList convert(Collection c) { - ImmutableList result = ImmutableSLList.nil(); + protected static ImmutableList convert(Collection c) { + ImmutableList result = ImmutableSLList.nil(); for (LocationVariable var : c) { result = result.append(var); } @@ -309,34 +314,21 @@ public Position getEndPosition() { /** * {@inheritDoc} + * + * @return */ @Override - public void fillSaveProperties(Properties properties) { - super.fillSaveProperties(properties); + public Configuration createLoaderConfig() { + var c = super.createLoaderConfig(); if (getStartPosition() != null) { - properties.setProperty("startLine", getStartPosition().line() + ""); - properties.setProperty("startColumn", getStartPosition().column() + ""); + c.set(START_LINE, getStartPosition().line() + ""); + c.set(START_COLUMN, getStartPosition().column() + ""); } if (getEndPosition() != null) { - properties.setProperty("endLine", getEndPosition().line() + ""); - properties.setProperty("endColumn", getEndPosition().column() + ""); + c.set(END_LINE, getEndPosition().line() + ""); + c.set(END_COLUMN, getEndPosition().column() + ""); } - } - - /** - * Instantiates a new proof obligation with the given settings. - * - * @param initConfig The already load {@link InitConfig}. - * @param properties The settings of the proof obligation to instantiate. - * @return The instantiated proof obligation. - * @throws IOException Occurred Exception. - */ - public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) - throws IOException { - return new LoadedPOContainer(new ProgramMethodSubsetPO(initConfig, getName(properties), - getProgramMethod(initConfig, properties), getPrecondition(properties), - getStartPosition(properties), getEndPosition(properties), - isAddUninterpretedPredicate(properties), isAddSymbolicExecutionLabel(properties))); + return c; } /** @@ -346,12 +338,12 @@ public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties prope * @return The defined start {@link Position}. * @throws IOException Occurred Exception if it was not possible to read the start position. */ - protected static Position getStartPosition(Properties properties) throws IOException { - String line = properties.getProperty("startLine"); + protected static Position getStartPosition(Configuration properties) throws IOException { + String line = properties.getString(START_LINE); if (line == null || line.isEmpty()) { throw new IOException("Start line property \"startLine\" is not available or empty."); } - String column = properties.getProperty("startColumn"); + String column = properties.getString(START_COLUMN); if (column == null || column.isEmpty()) { throw new IOException( "Start column property \"startColumn\" is not available or empty."); @@ -384,12 +376,12 @@ protected static Position getStartPosition(Properties properties) throws IOExcep * @return The defined end {@link Position}. * @throws IOException Occurred Exception if it was not possible to read the end position. */ - protected static Position getEndPosition(Properties properties) throws IOException { - String line = properties.getProperty("endLine"); + protected static Position getEndPosition(Configuration properties) throws IOException { + String line = properties.getString(END_LINE); if (line == null || line.isEmpty()) { throw new IOException("End line property \"endLine\" is not available or empty."); } - String column = properties.getProperty("endColumn"); + String column = properties.getString(END_COLUMN); if (column == null || column.isEmpty()) { throw new IOException("End column property \"endColumn\" is not available or empty."); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPOLoader.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPOLoader.java new file mode 100644 index 00000000000..0ce8cb402c8 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPOLoader.java @@ -0,0 +1,48 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.symbolic_execution.po; + +import java.io.IOException; + +import de.uka.ilkd.key.proof.init.*; +import de.uka.ilkd.key.proof.init.loader.ProofObligationLoader; +import de.uka.ilkd.key.settings.Configuration; + +import org.jspecify.annotations.NullMarked; + +/** + * @author Alexander Weigl + * @version 1 (28.12.23) + */ +@NullMarked +public class ProgramMethodSubsetPOLoader implements ProofObligationLoader { + /** + * Instantiates a new proof obligation with the given settings. + * + * @param initConfig The already loaded {@link InitConfig}. + * @param properties The settings of the proof obligation to instantiate. + * @return The instantiated proof obligation. + * @throws IOException Occurred Exception. + */ + @Override + public IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, + Configuration properties) throws IOException { + return new IPersistablePO.LoadedPOContainer( + new ProgramMethodSubsetPO(initConfig, AbstractPO.getName(properties), + ProgramMethodPO.getProgramMethod(initConfig, properties), + ProgramMethodPO.getPrecondition(properties), + ProgramMethodSubsetPO.getStartPosition(properties), + ProgramMethodSubsetPO.getEndPosition(properties), + AbstractOperationPO.isAddUninterpretedPredicate(properties), + AbstractOperationPO.isAddSymbolicExecutionLabel(properties))); + } + + @Override + public boolean handles(String identifier) { + return ProgramMethodSubsetPO.class.getName().equals(identifier) + || ProgramMethodSubsetPO.class.getSimpleName().equals(identifier) + || getClass().getName().equals(identifier) + || getClass().getSimpleName().equals(identifier); + } +} diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java index 6c1a1fa4212..6c1fc13fb94 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java @@ -128,9 +128,8 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { /** * {@inheritDoc} */ - @NonNull @Override - public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) + public @NonNull ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException { try { // Extract required Terms from goal diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java index 727b69d9f19..2f00a4a8941 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java @@ -189,9 +189,8 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { /** * {@inheritDoc} */ - @NonNull @Override - public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) + public @NonNull ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException { try { // Extract required Terms from goal diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java index 639365d2b37..d997436ad8e 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java @@ -32,6 +32,7 @@ import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -57,10 +58,10 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea private String conditionString; /** - * A list of {@link ProgramVariable}s containing all variables that were parsed and have to be + * A list of {@link LocationVariable}s containing all variables that were parsed and have to be * possibly replaced during runtime. */ - private ImmutableList varsForCondition; + private ImmutableList varsForCondition; /** * The KeYJavaType of the container of the element associated with the breakpoint. @@ -76,7 +77,7 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea * A {@link Map} mapping from relevant variables for the condition to their runtime equivalent * in KeY */ - private Map variableNamingMap; + private Map variableNamingMap; /** * The list of parameter variables of the method that contains the associated breakpoint @@ -84,9 +85,9 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea private final Set paramVars; /** - * A {@link ProgramVariable} representing the instance the class KeY is working on + * A {@link LocationVariable} representing the instance the class KeY is working on */ - private ProgramVariable selfVar; + private LocationVariable selfVar; /** * The {@link IProgramMethod} this Breakpoint lies within @@ -162,14 +163,14 @@ private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node, * * @return the cloned map */ - private Map getOldMap() { - Map oldMap = new HashMap<>(); - for (Entry svSubstituteSVSubstituteEntry : getVariableNamingMap() + private Map getOldMap() { + Map oldMap = new HashMap<>(); + for (Entry svSubstituteSVSubstituteEntry : getVariableNamingMap() .entrySet()) { Entry oldEntry = svSubstituteSVSubstituteEntry; - if (oldEntry.getKey() instanceof SVSubstitute - && oldEntry.getValue() instanceof SVSubstitute) { - oldMap.put((SVSubstitute) oldEntry.getKey(), (SVSubstitute) oldEntry.getValue()); + if (oldEntry.getKey() instanceof SyntaxElement + && oldEntry.getValue() instanceof SyntaxElement) { + oldMap.put((SyntaxElement) oldEntry.getKey(), (SyntaxElement) oldEntry.getValue()); } } return oldMap; @@ -200,7 +201,7 @@ private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScop * @param oldMap the oldMap variableNamings */ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope, - Map oldMap, RuleApp ruleApp) { + Map oldMap, RuleApp ruleApp) { // look for renamings KeY did boolean found = false; // get current renaming tables @@ -215,7 +216,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, .getHashMap().entrySet()) { Entry entry = value; if (entry.getKey() instanceof LocationVariable - && entry.getValue() instanceof SVSubstitute) { + && entry.getValue() instanceof SyntaxElement) { if ((VariableNamer.getBasename(((LocationVariable) entry.getKey()).name())) .equals(varForCondition.name()) && ((LocationVariable) entry.getKey()).name().toString() @@ -229,7 +230,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, // add new value toKeep.add((LocationVariable) entry.getValue()); getVariableNamingMap().put(varForCondition, - (SVSubstitute) entry.getValue()); + (SyntaxElement) entry.getValue()); found = true; break; } else if (inScope && ((LocationVariable) entry.getKey()).name() @@ -242,7 +243,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, // add new value toKeep.add((LocationVariable) entry.getValue()); getVariableNamingMap().put(varForCondition, - (SVSubstitute) entry.getValue()); + (SyntaxElement) entry.getValue()); found = true; break; } @@ -263,7 +264,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, protected void refreshVarMaps(RuleApp ruleApp, Node node) { boolean inScope = isInScope(node); // collect old values - Map oldMap = getOldMap(); + Map oldMap = getOldMap(); // put values into map which have to be replaced for (ProgramVariable varForCondition : getVarsForCondition()) { // put global variables only done when a variable is instantiated by @@ -291,14 +292,14 @@ private Term computeTermForCondition(String condition) { setSelfVar(new LocationVariable( new ProgramElementName(getProof().getServices().getTermBuilder().newName("self")), containerType, null, false, false)); - ImmutableList varsForCondition = ImmutableSLList.nil(); + ImmutableList varsForCondition = ImmutableSLList.nil(); if (getPm() != null) { // collect parameter variables for (ParameterDeclaration pd : getPm().getParameters()) { for (VariableSpecification vs : pd.getVariables()) { this.paramVars.add((LocationVariable) vs.getProgramVariable()); varsForCondition = - varsForCondition.append((ProgramVariable) vs.getProgramVariable()); + varsForCondition.append((LocationVariable) vs.getProgramVariable()); } } // Collect local variables @@ -313,7 +314,7 @@ private Term computeTermForCondition(String condition) { } JavaInfo info = getProof().getServices().getJavaInfo(); ImmutableList kjts = info.getAllSupertypes(containerType); - ImmutableList globalVars = ImmutableSLList.nil(); + ImmutableList globalVars = ImmutableSLList.nil(); for (KeYJavaType kjtloc : kjts) { if (kjtloc.getJavaType() instanceof TypeDeclaration) { ImmutableList fields = @@ -322,7 +323,7 @@ private Term computeTermForCondition(String condition) { if ((kjtloc.equals(containerType) || !field.isPrivate()) && !((LocationVariable) field.getProgramVariable()).isImplicit()) { globalVars = - globalVars.append((ProgramVariable) field.getProgramVariable()); + globalVars.append((LocationVariable) field.getProgramVariable()); } } } @@ -423,10 +424,10 @@ public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, P */ protected abstract boolean isInScopeForCondition(Node node); - private ImmutableList saveAddVariable(LocationVariable x, - ImmutableList varsForCondition) { + private ImmutableList saveAddVariable(LocationVariable x, + ImmutableList varsForCondition) { boolean contains = false; - for (ProgramVariable paramVar : varsForCondition) { + for (var paramVar : varsForCondition) { if (paramVar.toString().equals(x.toString())) { contains = true; break; @@ -498,42 +499,42 @@ public Set getToKeep() { /** * @return the variableNamingMap */ - public Map getVariableNamingMap() { + public Map getVariableNamingMap() { return variableNamingMap; } /** * @param variableNamingMap the variableNamingMap to set */ - public void setVariableNamingMap(Map variableNamingMap) { + public void setVariableNamingMap(Map variableNamingMap) { this.variableNamingMap = variableNamingMap; } /** * @return the selfVar */ - public ProgramVariable getSelfVar() { + public LocationVariable getSelfVar() { return selfVar; } /** * @param selfVar the selfVar to set */ - public void setSelfVar(ProgramVariable selfVar) { + public void setSelfVar(LocationVariable selfVar) { this.selfVar = selfVar; } /** * @return the varsForCondition */ - public ImmutableList getVarsForCondition() { + public ImmutableList getVarsForCondition() { return varsForCondition; } /** * @param varsForCondition the varsForCondition to set */ - public void setVarsForCondition(ImmutableList varsForCondition) { + public void setVarsForCondition(ImmutableList varsForCondition) { this.varsForCondition = varsForCondition; } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java index 0be6244d625..b61f4959c11 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java @@ -76,7 +76,7 @@ import org.slf4j.LoggerFactory; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; -import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; /** * Provides utility methods for symbolic execution with KeY. @@ -2686,7 +2686,7 @@ private static boolean checkReplaceTerm(Term toCheck, PosInOccurrence posInOccur Term replaceTerm) { Term termAtPio = followPosInOccurrence(posInOccurrence, toCheck); if (termAtPio != null) { - return termAtPio.equalsModProperty(replaceTerm, RENAMING_PROPERTY); + return termAtPio.equalsModProperty(replaceTerm, RENAMING_TERM_PROPERTY); } else { return false; } @@ -4141,7 +4141,7 @@ public static boolean lazyComputeIsAdditionalBranchVerified(Node node) { Set additinalPredicates = AbstractOperationPO.getAdditionalUninterpretedPredicates(node.proof()); // Check if node can be treated as verified/closed - if (!CollectionUtil.isEmpty(additinalPredicates)) { + if (additinalPredicates != null && !additinalPredicates.isEmpty()) { boolean verified = true; Iterator leafsIter = node.leavesIterator(); while (verified && leafsIter.hasNext()) { diff --git a/key.core.symbolic_execution/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader b/key.core.symbolic_execution/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader new file mode 100644 index 00000000000..3abacee7b1f --- /dev/null +++ b/key.core.symbolic_execution/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader @@ -0,0 +1,2 @@ +de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPOLoader +de.uka.ilkd.key.symbolic_execution.po.ProgramMethodSubsetPOLoader \ No newline at end of file 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/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java index 26b8bcedd61..49a2d95a902 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.util; import java.io.File; +import java.util.HashMap; import java.util.Map; import de.uka.ilkd.key.control.KeYEnvironment; @@ -148,8 +149,12 @@ public void test2GetAndSetChoiceSetting() { // Make sure that all other settings are unchanged. Map changedSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - defaultSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue); - Assertions.assertEquals(defaultSettings, changedSettings); + + Map expectedSettings = new HashMap<>(); + expectedSettings.putAll(defaultSettings); + expectedSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue); + + Assertions.assertEquals(expectedSettings, changedSettings); } finally { if (originalValue != null) { SymbolicExecutionUtil.setChoiceSetting( diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest.proof index d4389eb8644..43750c5c0fc 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest.proof @@ -44,14 +44,13 @@ \javaSource "."; -\proofObligation "#Proof Obligation Settings -#Tue Jul 25 22:57:12 CEST 2023 -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -contract=AllNodeTypesTest[AllNodeTypesTest\\:\\:main(AllNodeTypesTest)].JML normal_behavior operation contract.0 -name=AllNodeTypesTest[AllNodeTypesTest\\:\\:main(AllNodeTypesTest)].JML normal_behavior operation contract.0 -"; +\proofObligation { + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract": "AllNodeTypesTest[AllNodeTypesTest::main(AllNodeTypesTest)].JML normal_behavior operation contract.0", + "name": "AllNodeTypesTest[AllNodeTypesTest::main(AllNodeTypesTest)].JML normal_behavior operation contract.0", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile.proof index 6b49f1d2097..154868d7e2c 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile.proof @@ -44,13 +44,12 @@ \javaSource "."; -\proofObligation "#Proof Obligation Settings -#Tue Jul 25 22:57:42 CEST 2023 -addSymbolicExecutionLabel=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -contract=AllNodeTypesTest[AllNodeTypesTest\\:\\:main(AllNodeTypesTest)].JML normal_behavior operation contract.0 -name=AllNodeTypesTest[AllNodeTypesTest\\:\\:main(AllNodeTypesTest)].JML normal_behavior operation contract.0 -"; +\proofObligation { + "addSymbolicExecutionLabel": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract": "AllNodeTypesTest[AllNodeTypesTest::main(AllNodeTypesTest)].JML normal_behavior operation contract.0", + "name": "AllNodeTypesTest[AllNodeTypesTest::main(AllNodeTypesTest)].JML normal_behavior operation contract.0", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile_NoOneStepSimplification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile_NoOneStepSimplification.proof index b86f011358b..e7857b0573a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile_NoOneStepSimplification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile_NoOneStepSimplification.proof @@ -42,13 +42,12 @@ \javaSource "."; -\proofObligation "#Proof Obligation Settings -#Tue Jul 25 22:58:04 CEST 2023 -addSymbolicExecutionLabel=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -contract=AllNodeTypesTest[AllNodeTypesTest\\:\\:main(AllNodeTypesTest)].JML normal_behavior operation contract.0 -name=AllNodeTypesTest[AllNodeTypesTest\\:\\:main(AllNodeTypesTest)].JML normal_behavior operation contract.0 -"; +\proofObligation { + "addSymbolicExecutionLabel": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract": "AllNodeTypesTest[AllNodeTypesTest::main(AllNodeTypesTest)].JML normal_behavior operation contract.0", + "name": "AllNodeTypesTest[AllNodeTypesTest::main(AllNodeTypesTest)].JML normal_behavior operation contract.0", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/assumesUserInputTest/test/AssumesUserInputTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/assumesUserInputTest/test/AssumesUserInputTest.proof index f457ccb5846..beaa3a48728 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/assumesUserInputTest/test/AssumesUserInputTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/assumesUserInputTest/test/AssumesUserInputTest.proof @@ -50,14 +50,13 @@ }; } -\proofObligation "#Proof Obligation Settings -#Thu Jan 22 14:33:50 CET 2015 -name=AssumesUserInputTest[AssumesUserInputTest\\:\\:min(int,int,int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=AssumesUserInputTest[AssumesUserInputTest\\:\\:min(int,int,int)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "AssumesUserInputTest[AssumesUserInputTest::min(int,int,int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "AssumesUserInputTest[AssumesUserInputTest::min(int,int,int)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 94% 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 6a45f67f7b0..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 16:07:42 CEST 2016 -name=BlockContractAssignableEverything[BlockContractAssignableEverything\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractAssignableEverything[BlockContractAssignableEverything\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -150,7 +149,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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 95% 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 6592986d5af..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 16:39:35 CEST 2016 -name=BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -172,7 +171,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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 95% 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 e8cd6d684ce..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 16:36:39 CEST 2016 -name=BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -178,7 +177,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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/blockContractParamRemaned/test/BlockContractParamRemaned.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractParamRemaned/test/BlockContractParamRemaned.proof index 1ddd9b45976..c6b6189c84d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractParamRemaned/test/BlockContractParamRemaned.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractParamRemaned/test/BlockContractParamRemaned.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 15:01:02 CET 2018 -name=BlockContractParamRemaned[BlockContractParamRemaned\\:\\:main(int,int)].JML normal_behavior operation contract.0 -contract=BlockContractParamRemaned[BlockContractParamRemaned\\:\\:main(int,int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractParamRemaned[BlockContractParamRemaned::main(int,int)].JML normal_behavior operation contract.0", + "contract": "BlockContractParamRemaned[BlockContractParamRemaned::main(int,int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractPreconditionNotVerified/test/BlockContractPreconditionNotVerified.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractPreconditionNotVerified/test/BlockContractPreconditionNotVerified.proof index a1059062509..9108a91bc3d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractPreconditionNotVerified/test/BlockContractPreconditionNotVerified.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractPreconditionNotVerified/test/BlockContractPreconditionNotVerified.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 14:11:53 CET 2018 -name=BlockContractPreconditionNotVerified[BlockContractPreconditionNotVerified\\:\\:main(int)].JML normal_behavior operation contract.0 -contract=BlockContractPreconditionNotVerified[BlockContractPreconditionNotVerified\\:\\:main(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractPreconditionNotVerified[BlockContractPreconditionNotVerified::main(int)].JML normal_behavior operation contract.0", + "contract": "BlockContractPreconditionNotVerified[BlockContractPreconditionNotVerified::main(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractThisTest/test/BlockContractThisTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractThisTest/test/BlockContractThisTest.proof index f28a50c1ef3..3e5b62fdd6c 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractThisTest/test/BlockContractThisTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractThisTest/test/BlockContractThisTest.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 14:11:48 CET 2018 -name=BlockContractThisTest[BlockContractThisTest\\:\\:magic()].JML normal_behavior operation contract.0 -contract=BlockContractThisTest[BlockContractThisTest\\:\\:magic()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractThisTest[BlockContractThisTest::magic()].JML normal_behavior operation contract.0", + "contract": "BlockContractThisTest[BlockContractThisTest::magic()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractVarRenamedLater/test/BlockContractVarRenamedLater.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractVarRenamedLater/test/BlockContractVarRenamedLater.proof index 03a944bec4b..5688f88d4ef 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractVarRenamedLater/test/BlockContractVarRenamedLater.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractVarRenamedLater/test/BlockContractVarRenamedLater.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 14:11:43 CET 2018 -name=BlockContractVarRenamedLater[BlockContractVarRenamedLater\\:\\:main()].JML normal_behavior operation contract.0 -contract=BlockContractVarRenamedLater[BlockContractVarRenamedLater\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractVarRenamedLater[BlockContractVarRenamedLater::main()].JML normal_behavior operation contract.0", + "contract": "BlockContractVarRenamedLater[BlockContractVarRenamedLater::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithException/test/BlockContractWithException.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithException/test/BlockContractWithException.proof index 316538faf05..d0364a64ea7 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithException/test/BlockContractWithException.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithException/test/BlockContractWithException.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 10:58:28 CEST 2016 -name=BlockContractWithException[BlockContractWithException\\:\\:main(int)].JML exceptional_behavior operation contract.0 -contract=BlockContractWithException[BlockContractWithException\\:\\:main(int)].JML exceptional_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractWithException[BlockContractWithException::main(int)].JML exceptional_behavior operation contract.0", + "contract": "BlockContractWithException[BlockContractWithException::main(int)].JML exceptional_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithExceptionPostconditionNotVerified/test/BlockContractWithExceptionPostconditionNotVerified.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithExceptionPostconditionNotVerified/test/BlockContractWithExceptionPostconditionNotVerified.proof index d7fa0fe669e..020a5b07940 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithExceptionPostconditionNotVerified/test/BlockContractWithExceptionPostconditionNotVerified.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithExceptionPostconditionNotVerified/test/BlockContractWithExceptionPostconditionNotVerified.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 10:58:31 CEST 2016 -name=BlockContractWithExceptionPostconditionNotVerified[BlockContractWithExceptionPostconditionNotVerified\\:\\:main(int)].JML exceptional_behavior operation contract.0 -contract=BlockContractWithExceptionPostconditionNotVerified[BlockContractWithExceptionPostconditionNotVerified\\:\\:main(int)].JML exceptional_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractWithExceptionPostconditionNotVerified[BlockContractWithExceptionPostconditionNotVerified::main(int)].JML exceptional_behavior operation contract.0", + "contract": "BlockContractWithExceptionPostconditionNotVerified[BlockContractWithExceptionPostconditionNotVerified::main(int)].JML exceptional_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturn/test/BlockContractWithReturn.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturn/test/BlockContractWithReturn.proof index fe8f6a0e33e..8f51c9285d4 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturn/test/BlockContractWithReturn.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturn/test/BlockContractWithReturn.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 14:09:27 CET 2018 -name=BlockContractWithReturn[BlockContractWithReturn\\:\\:main(int)].JML normal_behavior operation contract.0 -contract=BlockContractWithReturn[BlockContractWithReturn\\:\\:main(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractWithReturn[BlockContractWithReturn::main(int)].JML normal_behavior operation contract.0", + "contract": "BlockContractWithReturn[BlockContractWithReturn::main(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturnPostconditionNotVerified/test/BlockContractWithReturnPostconditionNotVerified.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturnPostconditionNotVerified/test/BlockContractWithReturnPostconditionNotVerified.proof index 26ca7f9bfd6..949e03929fe 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturnPostconditionNotVerified/test/BlockContractWithReturnPostconditionNotVerified.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractWithReturnPostconditionNotVerified/test/BlockContractWithReturnPostconditionNotVerified.proof @@ -43,13 +43,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 14:08:06 CET 2018 -name=BlockContractWithReturnPostconditionNotVerified[BlockContractWithReturnPostconditionNotVerified\\:\\:main(int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractWithReturnPostconditionNotVerified[BlockContractWithReturnPostconditionNotVerified\\:\\:main(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractWithReturnPostconditionNotVerified[BlockContractWithReturnPostconditionNotVerified::main(int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractWithReturnPostconditionNotVerified[BlockContractWithReturnPostconditionNotVerified::main(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/configurationExtractorExistsQuantifierTest/test/ExistsQuantifierTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/configurationExtractorExistsQuantifierTest/test/ExistsQuantifierTest.proof index 77b4ed8be80..5ada012d310 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/configurationExtractorExistsQuantifierTest/test/ExistsQuantifierTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/configurationExtractorExistsQuantifierTest/test/ExistsQuantifierTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 18 11:12:58 CET 2016 -name=ExistsQuantifierTest[ExistsQuantifierTest\\:\\:compute()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ExistsQuantifierTest[ExistsQuantifierTest\\:\\:compute()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ExistsQuantifierTest[ExistsQuantifierTest::compute()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ExistsQuantifierTest[ExistsQuantifierTest::compute()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/fullqualifiedTypeNamesTest/test/my/packageName/TestProgramMethodSubsetPO9033468379300181045.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/fullqualifiedTypeNamesTest/test/my/packageName/TestProgramMethodSubsetPO9033468379300181045.proof index 16b60f8006e..63e5e21c560 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/fullqualifiedTypeNamesTest/test/my/packageName/TestProgramMethodSubsetPO9033468379300181045.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/fullqualifiedTypeNamesTest/test/my/packageName/TestProgramMethodSubsetPO9033468379300181045.proof @@ -45,13 +45,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Thu Oct 04 18:18:29 CEST 2012 -name=complicatedInnerMethod -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=my.packageName.TheClass.TheInnerClass\\#complicatedInnerMethod(my.packageName.TheClass, int, boolean, java.lang.String, java.lang.Object[], my.packageName.sub.AnotherClass) -"; +\proofObligation { + "name": "complicatedInnerMethod", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "my.packageName.TheClass.TheInnerClass#complicatedInnerMethod(my.packageName.TheClass, int, boolean, java.lang.String, java.lang.Object[], my.packageName.sub.AnotherClass)", + } \proof { (keyLog "0" (keyUser "IStudent" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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/joinTest/test/JoinTestAfterAssignment.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterAssignment.proof index 3449c811022..fd5cb648b12 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterAssignment.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterAssignment.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Apr 07 16:04:13 CEST 2017 -name=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -contract=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "contract": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchCondition.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchCondition.proof index 972a9596247..d13ad1a0289 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchCondition.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchCondition.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Apr 07 16:28:34 CEST 2017 -name=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof index 0343f322e96..82bc5ea2e6d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Apr 07 16:37:34 CEST 2017 -name=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalAndSubgoals.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalAndSubgoals.proof index be86bed6eea..ec082093779 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalAndSubgoals.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalAndSubgoals.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Apr 07 16:38:26 CEST 2017 -name=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalNotVerified.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalNotVerified.proof index 61e204a76b1..4cca643eea6 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalNotVerified.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/joinTest/test/JoinTestAfterBranchConditionWithWeakeningGoalNotVerified.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Apr 07 16:42:20 CEST 2017 -name=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/magic42/test/Magic42.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/magic42/test/Magic42.proof index 0e24f7297bb..f109d8cb533 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/magic42/test/Magic42.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/magic42/test/Magic42.proof @@ -40,14 +40,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Jun 25 11:46:39 CEST 2014 -name=compute(int) -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=Magic42\\#compute(int) -"; +\proofObligation { + "name": "compute(int)", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "Magic42#compute(int)", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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/truthValueAddingOfLabeledSubtree/test/ImmutableList.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAddingOfLabeledSubtree/test/ImmutableList.proof index d24721f51e6..1982c79f45a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAddingOfLabeledSubtree/test/ImmutableList.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAddingOfLabeledSubtree/test/ImmutableList.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 23 14:12:50 CET 2016 -name=ImmutableList[ImmutableList\\:\\:down2()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ImmutableList[ImmutableList\\:\\:down2()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ImmutableList[ImmutableList::down2()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ImmutableList[ImmutableList::down2()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAnd/test/And3_replaceKnown.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAnd/test/And3_replaceKnown.proof index e439b8ec92e..4f7838e7f88 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAnd/test/And3_replaceKnown.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueAnd/test/And3_replaceKnown.proof @@ -41,12 +41,11 @@ \javaSource ".."; -\proofObligation "#Proof Obligation Settings -#Mon Sep 14 10:33:14 CEST 2015 -name=truthValueEvaluation.And[truthValueEvaluation.And\\:\\:doNothing(boolean,boolean)].JML normal_behavior operation contract.0 -contract=truthValueEvaluation.And[truthValueEvaluation.And\\:\\:doNothing(boolean,boolean)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "truthValueEvaluation.And[truthValueEvaluation.And::doNothing(boolean,boolean)].JML normal_behavior operation contract.0", + "contract": "truthValueEvaluation.And[truthValueEvaluation.And::doNothing(boolean,boolean)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhile.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhile.proof index f3bf091481d..2ec885204f2 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhile.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhile.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Thu Jan 29 12:09:31 CET 2015 -name=ArraySumWhile[ArraySumWhile\\:\\:sum([I)].JML operation contract.0 -addSymbolicExecutionLabel=true -contract=ArraySumWhile[ArraySumWhile\\:\\:sum([I)].JML operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArraySumWhile[ArraySumWhile::sum([I)].JML operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArraySumWhile[ArraySumWhile::sum([I)].JML operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhileNoOneStepSimplification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhileNoOneStepSimplification.proof index a0645245a93..142d6dd31cb 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhileNoOneStepSimplification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArraySumWhile/test/ArraySumWhileNoOneStepSimplification.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Thu Jan 29 12:09:59 CET 2015 -name=ArraySumWhile[ArraySumWhile\\:\\:sum([I)].JML operation contract.0 -addSymbolicExecutionLabel=true -contract=ArraySumWhile[ArraySumWhile\\:\\:sum([I)].JML operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArraySumWhile[ArraySumWhile::sum([I)].JML operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArraySumWhile[ArraySumWhile::sum([I)].JML operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtil.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtil.proof index 65a2a51e323..eaf5b5b41fd 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtil.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtil.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jan 16 12:05:42 CET 2015 -name=ArrayUtil[ArrayUtil\\:\\:indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayUtil[ArrayUtil\\:\\:indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayUtil[ArrayUtil::indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayUtil[ArrayUtil::indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtilNoOneStepSimplification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtilNoOneStepSimplification.proof index 3b230790215..aaa681d4303 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtilNoOneStepSimplification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueArrayUtil/test/ArrayUtilNoOneStepSimplification.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jan 16 12:06:05 CET 2015 -name=ArrayUtil[ArrayUtil\\:\\:indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayUtil[ArrayUtil\\:\\:indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayUtil[ArrayUtil::indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayUtil[ArrayUtil::indexOf([Ljava.lang.Object,ArrayUtil.Filter)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueBlockContractMagic42/test/BlockContractMagic42.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueBlockContractMagic42/test/BlockContractMagic42.proof index b3817e1cb88..9908b1fc393 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueBlockContractMagic42/test/BlockContractMagic42.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueBlockContractMagic42/test/BlockContractMagic42.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Thu May 19 14:52:54 CEST 2016 -name=BlockContractMagic42[BlockContractMagic42\\:\\:magic()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractMagic42[BlockContractMagic42\\:\\:magic()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractMagic42[BlockContractMagic42::magic()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractMagic42[BlockContractMagic42::magic()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueDifferentBranchesTest/test/DifferentBranchesTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueDifferentBranchesTest/test/DifferentBranchesTest.proof index 8cbba266612..7baf78c9ccb 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueDifferentBranchesTest/test/DifferentBranchesTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueDifferentBranchesTest/test/DifferentBranchesTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 11:01:54 CEST 2016 -name=DifferentBranchesTest[DifferentBranchesTest\\:\\:main([I)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=DifferentBranchesTest[DifferentBranchesTest\\:\\:main([I)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "DifferentBranchesTest[DifferentBranchesTest::main([I)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "DifferentBranchesTest[DifferentBranchesTest::main([I)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExample.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExample.proof index bb022f736df..70e03743fe1 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExample.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExample.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Tue Jan 06 11:14:35 CET 2015 -name=EquivExample[EquivExample\\:\\:equivExample()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=EquivExample[EquivExample\\:\\:equivExample()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "EquivExample[EquivExample::equivExample()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "EquivExample[EquivExample::equivExample()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExampleNoOneStepSimplification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExampleNoOneStepSimplification.proof index 8eaef0abfe4..4b287b00e23 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExampleNoOneStepSimplification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueEquivExample/test/EquivExampleNoOneStepSimplification.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Dec 05 16:22:17 CET 2014 -name=EquivExample[EquivExample\\:\\:equivExample()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=EquivExample[EquivExample\\:\\:equivExample()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "EquivExample[EquivExample::equivExample()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "EquivExample[EquivExample::equivExample()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 98% 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 c21da623cbe..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 @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 11:01:14 CEST 2016 -name=ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest\\:\\:main()].JML exceptional_behavior operation contract.0 -contract=ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest\\:\\:main()].JML exceptional_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "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", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 98% 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 3d6ce6a6b6d..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 @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 11:01:31 CEST 2016 -name=ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest\\:\\:main()].JML exceptional_behavior operation contract.0 -contract=ExceptinalAssignableNothingTest[ExceptinalAssignableNothingTest\\:\\:main()].JML exceptional_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "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", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueLabelBelowUpdatesDifferentToApplicationTerm/test/TwoBranch.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueLabelBelowUpdatesDifferentToApplicationTerm/test/TwoBranch.proof index bf7339ab1cf..2f250331bd7 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueLabelBelowUpdatesDifferentToApplicationTerm/test/TwoBranch.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueLabelBelowUpdatesDifferentToApplicationTerm/test/TwoBranch.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 08 11:07:54 CEST 2016 -name=OneBranch[OneBranch\\:\\:magic()].JML normal_behavior operation contract.0 -contract=OneBranch[OneBranch\\:\\:magic()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "OneBranch[OneBranch::magic()].JML normal_behavior operation contract.0", + "contract": "OneBranch[OneBranch::magic()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 99% 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 index e80979c8317..753c78225b9 100644 --- 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 @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 11:02:13 CEST 2016 -name=ExampleInstance[ExampleInstance\\:\\:magic()].JML normal_behavior operation contract.0 -contract=ExampleInstance[ExampleInstance\\:\\:magic()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ExampleInstance[ExampleInstance::magic()].JML normal_behavior operation contract.0", + "contract": "ExampleInstance[ExampleInstance::magic()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueMyInteger/test/MyInteger.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueMyInteger/test/MyInteger.proof index 2f8538773fe..2b6b2cd00bc 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueMyInteger/test/MyInteger.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueMyInteger/test/MyInteger.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:13:45 CEST 2016 -name=MyInteger[MyInteger\\:\\:add(MyInteger)].JML normal_behavior operation contract.0 -contract=MyInteger[MyInteger\\:\\:add(MyInteger)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "MyInteger[MyInteger::add(MyInteger)].JML normal_behavior operation contract.0", + "contract": "MyInteger[MyInteger::add(MyInteger)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueNotLastEvaluationGivesTruthValue/test/NotLastEvaluationGivesTruthValue.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueNotLastEvaluationGivesTruthValue/test/NotLastEvaluationGivesTruthValue.proof index 8bae39424f9..bd2de896b8f 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueNotLastEvaluationGivesTruthValue/test/NotLastEvaluationGivesTruthValue.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueNotLastEvaluationGivesTruthValue/test/NotLastEvaluationGivesTruthValue.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Nov 26 17:47:38 CET 2014 -name=PredicateEvaluationComposedTerms[PredicateEvaluationComposedTerms\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=PredicateEvaluationComposedTerms[PredicateEvaluationComposedTerms\\:\\:main()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "PredicateEvaluationComposedTerms[PredicateEvaluationComposedTerms::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "PredicateEvaluationComposedTerms[PredicateEvaluationComposedTerms::main()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueRejectedFormula/test/LabelLostVerification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueRejectedFormula/test/LabelLostVerification.proof index 8d18b23fab4..17489a504d5 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueRejectedFormula/test/LabelLostVerification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueRejectedFormula/test/LabelLostVerification.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 23 17:07:21 CET 2016 -name=LabelLost[LabelLost\\:\\:magic(boolean,boolean)].JML normal_behavior operation contract.0 -contract=LabelLost[LabelLost\\:\\:magic(boolean,boolean)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "LabelLost[LabelLost::magic(boolean,boolean)].JML normal_behavior operation contract.0", + "contract": "LabelLost[LabelLost::magic(boolean,boolean)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication.proof index b77e36778a2..3c1c35f6a18 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jan 05 12:08:43 CET 2015 -name=SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication\\:\\:main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication\\:\\:main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication::main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication::main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication_NoOneStepSimplification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication_NoOneStepSimplification.proof index c0cca39743d..a86276ba48a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication_NoOneStepSimplification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleInstanceMethodContractApplication/test/SimpleInstanceMethodContractApplication_NoOneStepSimplification.proof @@ -44,14 +44,13 @@ \javaSource "."; -\proofObligation "#Proof Obligation Settings -#Fri Oct 22 15:04:52 CEST 2021 -addSymbolicExecutionLabel=true -contract=SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication\\:\\:main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0 -name=SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication\\:\\:main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -addUninterpretedPredicate=true -"; +\proofObligation { + "addSymbolicExecutionLabel": true, + "contract": "SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication::main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0", + "name": "SimpleInstanceMethodContractApplication[SimpleInstanceMethodContractApplication::main(SimpleInstanceMethodContractApplication)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "addUninterpretedPredicate": true, + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication.proof index 7abeffd0447..adfa4c3cde8 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jan 05 12:07:09 CET 2015 -name=SimpleMethodContractApplication[SimpleMethodContractApplication\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleMethodContractApplication[SimpleMethodContractApplication\\:\\:main()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleMethodContractApplication[SimpleMethodContractApplication::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleMethodContractApplication[SimpleMethodContractApplication::main()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication_NoOneStepSimplification.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication_NoOneStepSimplification.proof index 237c227fe97..3e645a675d6 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication_NoOneStepSimplification.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueSimpleMethodContractApplication/test/SimpleMethodContractApplication_NoOneStepSimplification.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jan 05 11:50:17 CET 2015 -name=SimpleMethodContractApplication[SimpleMethodContractApplication\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleMethodContractApplication[SimpleMethodContractApplication\\:\\:main()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleMethodContractApplication[SimpleMethodContractApplication::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleMethodContractApplication[SimpleMethodContractApplication::main()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsAccount/test/Account.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsAccount/test/Account.proof index 44c62813a4c..45f65e1a1ac 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsAccount/test/Account.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsAccount/test/Account.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jun 15 15:52:36 CEST 2015 -name=Account[Account\\:\\:checkAndWithdraw(int)].JML normal_behavior operation contract.0 -contract=Account[Account\\:\\:checkAndWithdraw(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "Account[Account::checkAndWithdraw(int)].JML normal_behavior operation contract.0", + "contract": "Account[Account::checkAndWithdraw(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsArrayUtil/test/ArrayUtil.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsArrayUtil/test/ArrayUtil.proof index cbaa90eb89e..25578e560d4 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsArrayUtil/test/ArrayUtil.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsArrayUtil/test/ArrayUtil.proof @@ -43,13 +43,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Mar 23 14:47:12 CET 2018 -name=ArrayUtil[ArrayUtil\\:\\:minIndex([I)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayUtil[ArrayUtil\\:\\:minIndex([I)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayUtil[ArrayUtil::minIndex([I)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayUtil[ArrayUtil::minIndex([I)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsCalendar/test/Calendar.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsCalendar/test/Calendar.proof index 6cbe5c68a39..55402cddab6 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsCalendar/test/Calendar.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsCalendar/test/Calendar.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 10:59:15 CEST 2016 -name=Calendar[Calendar\\:\\:addEntry(Calendar.Entry)].JML normal_behavior operation contract.0 -contract=Calendar[Calendar\\:\\:addEntry(Calendar.Entry)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "Calendar[Calendar::addEntry(Calendar.Entry)].JML normal_behavior operation contract.0", + "contract": "Calendar[Calendar::addEntry(Calendar.Entry)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsMyInteger/test/MyInteger.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsMyInteger/test/MyInteger.proof index e5db90a7fdb..d4e4e924833 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsMyInteger/test/MyInteger.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueUnderstandingProofsMyInteger/test/MyInteger.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:15:42 CEST 2016 -name=MyInteger[MyInteger\\:\\:add(MyInteger)].JML normal_behavior operation contract.0 -contract=MyInteger[MyInteger\\:\\:add(MyInteger)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "MyInteger[MyInteger::add(MyInteger)].JML normal_behavior operation contract.0", + "contract": "MyInteger[MyInteger::add(MyInteger)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueWeakeningTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueWeakeningTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof index 68b7591be42..c22993d69fc 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueWeakeningTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueWeakeningTest/test/JoinTestAfterBranchConditionWithWeakeningGoal.proof @@ -41,12 +41,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Apr 10 16:43:30 CEST 2017 -name=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -contract=JoinTest[JoinTest\\:\\:zero(int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "contract": "JoinTest[JoinTest::zero(int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/useLoopInvariantWithoutDecreasing/test/LoopInvArrayExample.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/useLoopInvariantWithoutDecreasing/test/LoopInvArrayExample.proof index f29091f8cb3..7757ffb1e98 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/useLoopInvariantWithoutDecreasing/test/LoopInvArrayExample.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/useLoopInvariantWithoutDecreasing/test/LoopInvArrayExample.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Jul 18 10:57:38 CEST 2016 -name=LoopInvArrayExample[LoopInvArrayExample\\:\\:setAllToOne()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=LoopInvArrayExample[LoopInvArrayExample\\:\\:setAllToOne()].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "LoopInvArrayExample[LoopInvArrayExample::setAllToOne()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "LoopInvArrayExample[LoopInvArrayExample::setAllToOne()].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMin.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMin.proof index 5c1d89624dd..3c894fb050d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMin.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMin.proof @@ -40,12 +40,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Aug 01 11:46:32 CEST 2014 -name=VerifyMin[VerifyMin\\:\\:min(int,int)].JML normal_behavior operation contract.0 -contract=VerifyMin[VerifyMin\\:\\:min(int,int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "VerifyMin[VerifyMin::min(int,int)].JML normal_behavior operation contract.0", + "contract": "VerifyMin[VerifyMin::min(int,int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMinTrueBranch.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMinTrueBranch.proof index 541dd7aa08b..c6184db908f 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMinTrueBranch.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyMin/test/VerifyMinTrueBranch.proof @@ -40,12 +40,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Aug 01 12:24:02 CEST 2014 -name=VerifyMin[VerifyMin\\:\\:min(int,int)].JML normal_behavior operation contract.0 -contract=VerifyMin[VerifyMin\\:\\:min(int,int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "VerifyMin[VerifyMin::min(int,int)].JML normal_behavior operation contract.0", + "contract": "VerifyMin[VerifyMin::min(int,int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyNumber/test/VerifyNumberNormal.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyNumber/test/VerifyNumberNormal.proof index e19bcb46af9..cd6829db36c 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyNumber/test/VerifyNumberNormal.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/verificationProofFile_VerifyNumber/test/VerifyNumberNormal.proof @@ -40,12 +40,11 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Aug 01 12:30:09 CEST 2014 -name=VerifyNumber[VerifyNumber\\:\\:equals(VerifyNumber)].JML normal_behavior operation contract.0 -contract=VerifyNumber[VerifyNumber\\:\\:equals(VerifyNumber)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "VerifyNumber[VerifyNumber::equals(VerifyNumber)].JML normal_behavior operation contract.0", + "contract": "VerifyNumber[VerifyNumber::equals(VerifyNumber)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasChanged/AliasChanged.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasChanged/AliasChanged.proof index 691bb4d580e..4250bd840af 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasChanged/AliasChanged.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasChanged/AliasChanged.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:18:57 CEST 2016 -name=AliasChanged[AliasChanged\\:\\:main(AliasChanged,AliasChanged)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=AliasChanged[AliasChanged\\:\\:main(AliasChanged,AliasChanged)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "AliasChanged[AliasChanged::main(AliasChanged,AliasChanged)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "AliasChanged[AliasChanged::main(AliasChanged,AliasChanged)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasNotAvailable/AliasNotAvailable.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasNotAvailable/AliasNotAvailable.proof index a1f1865b2ab..b7df477bdbf 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasNotAvailable/AliasNotAvailable.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasNotAvailable/AliasNotAvailable.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:19:25 CEST 2016 -name=AliasNotAvailable[AliasNotAvailable\\:\\:main(AliasNotAvailable,AliasNotAvailable)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=AliasNotAvailable[AliasNotAvailable\\:\\:main(AliasNotAvailable,AliasNotAvailable)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "AliasNotAvailable[AliasNotAvailable::main(AliasNotAvailable,AliasNotAvailable)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "AliasNotAvailable[AliasNotAvailable::main(AliasNotAvailable,AliasNotAvailable)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasedByExecutionTest/AliasedByExecution.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasedByExecutionTest/AliasedByExecution.proof index 1e935e882dc..b72665061e6 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasedByExecutionTest/AliasedByExecution.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasedByExecutionTest/AliasedByExecution.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Tue Mar 29 14:36:15 CEST 2016 -name=AliasedByExecution[AliasedByExecution\\:\\:magic(AliasedByExecution,AliasedByExecution)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=AliasedByExecution[AliasedByExecution\\:\\:magic(AliasedByExecution,AliasedByExecution)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "AliasedByExecution[AliasedByExecution::magic(AliasedByExecution,AliasedByExecution)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "AliasedByExecution[AliasedByExecution::magic(AliasedByExecution,AliasedByExecution)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasing/Aliasing.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasing/Aliasing.proof index f07f73b5a94..6d7c45a7306 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasing/Aliasing.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/aliasing/Aliasing.proof @@ -41,15 +41,14 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Feb 02 13:11:32 CET 2015 -name=main(Aliasing, Aliasing) -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -precondition=a \\!\\= null && b \\!\\= null -method=Aliasing\\#main(Aliasing, Aliasing) -"; +\proofObligation { + "name": "main(Aliasing, Aliasing)", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "precondition": "a != null && b != null", + "method": "Aliasing#main(Aliasing, Aliasing)", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexAsVariableFieldTest/ArrayIndexAsVariableFieldTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexAsVariableFieldTest/ArrayIndexAsVariableFieldTest.proof index be140c6d78b..b3275566e2d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexAsVariableFieldTest/ArrayIndexAsVariableFieldTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexAsVariableFieldTest/ArrayIndexAsVariableFieldTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Feb 20 14:12:10 CET 2015 -name=ArrayIndexAsVariableFieldTest[ArrayIndexAsVariableFieldTest\\:\\:main([LArrayIndexAsVariableFieldTest,ArrayIndexAsVariableFieldTest.Index)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayIndexAsVariableFieldTest[ArrayIndexAsVariableFieldTest\\:\\:main([LArrayIndexAsVariableFieldTest,ArrayIndexAsVariableFieldTest.Index)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayIndexAsVariableFieldTest[ArrayIndexAsVariableFieldTest::main([LArrayIndexAsVariableFieldTest,ArrayIndexAsVariableFieldTest.Index)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayIndexAsVariableFieldTest[ArrayIndexAsVariableFieldTest::main([LArrayIndexAsVariableFieldTest,ArrayIndexAsVariableFieldTest.Index)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsAfter/ArrayIndexSideeffectsAfter.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsAfter/ArrayIndexSideeffectsAfter.proof index eba97ab0be7..54ecd6ac628 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsAfter/ArrayIndexSideeffectsAfter.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsAfter/ArrayIndexSideeffectsAfter.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Feb 20 14:04:28 CET 2015 -name=ArrayIndexSideeffectsAfter[ArrayIndexSideeffectsAfter\\:\\:mainAfter([I,int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayIndexSideeffectsAfter[ArrayIndexSideeffectsAfter\\:\\:mainAfter([I,int)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayIndexSideeffectsAfter[ArrayIndexSideeffectsAfter::mainAfter([I,int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayIndexSideeffectsAfter[ArrayIndexSideeffectsAfter::mainAfter([I,int)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsBevore/ArrayIndexSideeffectsBevore.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsBevore/ArrayIndexSideeffectsBevore.proof index 9132158ab2d..e8e1b304ad1 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsBevore/ArrayIndexSideeffectsBevore.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexSideeffectsBevore/ArrayIndexSideeffectsBevore.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Feb 20 14:07:48 CET 2015 -name=ArrayIndexSideeffectsBevore[ArrayIndexSideeffectsBevore\\:\\:mainBevore([I,int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayIndexSideeffectsBevore[ArrayIndexSideeffectsBevore\\:\\:mainBevore([I,int)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayIndexSideeffectsBevore[ArrayIndexSideeffectsBevore::mainBevore([I,int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayIndexSideeffectsBevore[ArrayIndexSideeffectsBevore::mainBevore([I,int)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexVariableTest/ArrayIndexVariableTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexVariableTest/ArrayIndexVariableTest.proof index ee590d876f8..f2dbcf64df7 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexVariableTest/ArrayIndexVariableTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/arrayIndexVariableTest/ArrayIndexVariableTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Feb 20 14:09:49 CET 2015 -name=ArrayIndexVariableTest[ArrayIndexVariableTest\\:\\:main([LArrayIndexVariableTest,int)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=ArrayIndexVariableTest[ArrayIndexVariableTest\\:\\:main([LArrayIndexVariableTest,int)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "ArrayIndexVariableTest[ArrayIndexVariableTest::main([LArrayIndexVariableTest,int)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "ArrayIndexVariableTest[ArrayIndexVariableTest::main([LArrayIndexVariableTest,int)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 94% 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 6a45f67f7b0..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 16:07:42 CEST 2016 -name=BlockContractAssignableEverything[BlockContractAssignableEverything\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractAssignableEverything[BlockContractAssignableEverything\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractModifiableEverything[BlockContractModifiableEverything::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -150,7 +149,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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 95% 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 6592986d5af..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 16:39:35 CEST 2016 -name=BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -172,7 +171,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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 95% 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 e8cd6d684ce..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 16:36:39 CEST 2016 -name=BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -178,7 +177,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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/equivalenceClassesTest/Example.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example.proof index fa69f08b591..dc321749ffc 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Tue Mar 29 14:23:08 CEST 2016 -name=Example[Example\\:\\:magic(Example,Example)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=Example[Example\\:\\:magic(Example,Example)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "Example[Example::magic(Example,Example)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "Example[Example::magic(Example,Example)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example_NoOSS.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example_NoOSS.proof index 5f57780121c..6b7be1eeb09 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example_NoOSS.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/equivalenceClassesTest/Example_NoOSS.proof @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 13:40:52 CEST 2016 -name=Example[Example\\:\\:magic(Example,Example)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=Example[Example\\:\\:magic(Example,Example)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "Example[Example::magic(Example,Example)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "Example[Example::magic(Example,Example)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2/Figure2.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2/Figure2.proof index 5a76b8d5631..eec4ac3be56 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2/Figure2.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2/Figure2.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 20 00:06:56 CET 2019 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=Figure2\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "Figure2#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Instance/Figure2Instance.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Instance/Figure2Instance.proof index 8770f00b94d..ad3364dbb35 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Instance/Figure2Instance.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Instance/Figure2Instance.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Tue Mar 19 13:46:43 CET 2019 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=Figure2Instance\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "Figure2Instance#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Local/Figure2Local.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Local/Figure2Local.proof index 73b02eadc67..c91e4649451 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Local/Figure2Local.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Local/Figure2Local.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Tue Mar 19 23:43:13 CET 2019 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=Figure2Local\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "Figure2Local#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Param/Figure2Param.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Param/Figure2Param.proof index 90239c90cbd..b90dc803d77 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Param/Figure2Param.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/figure2Param/Figure2Param.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 20 00:03:03 CET 2019 -name=main(Figure2Param.A, Figure2Param.A, Figure2Param.B, Figure2Param.A, Figure2Param.B) -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=Figure2Param\\#main(Figure2Param.A, Figure2Param.A, Figure2Param.B, Figure2Param.A, Figure2Param.B) -"; +\proofObligation { + "name": "main(Figure2Param.A, Figure2Param.A, Figure2Param.B, Figure2Param.A, Figure2Param.B)", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "Figure2Param#main(Figure2Param.A, Figure2Param.A, Figure2Param.B, Figure2Param.A, Figure2Param.B)", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/instanceFieldsAliased/InstanceFieldsAliased.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/instanceFieldsAliased/InstanceFieldsAliased.proof index e1233d8801c..25ef6b133d9 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/instanceFieldsAliased/InstanceFieldsAliased.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/instanceFieldsAliased/InstanceFieldsAliased.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:20:51 CEST 2016 -name=InstanceFieldsAliased[InstanceFieldsAliased\\:\\:main(InstanceFieldsAliased,InstanceFieldsAliased)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=InstanceFieldsAliased[InstanceFieldsAliased\\:\\:main(InstanceFieldsAliased,InstanceFieldsAliased)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "InstanceFieldsAliased[InstanceFieldsAliased::main(InstanceFieldsAliased,InstanceFieldsAliased)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "InstanceFieldsAliased[InstanceFieldsAliased::main(InstanceFieldsAliased,InstanceFieldsAliased)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/intEndTest/IntEndTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/intEndTest/IntEndTest.proof index 704ad58b78a..4cd94700bd2 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/intEndTest/IntEndTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/intEndTest/IntEndTest.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Mar 26 14:08:49 CEST 2018 -name=main(int) -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=IntEndTest\\#main(int) -"; +\proofObligation { + "name": "main(int)", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "IntEndTest#main(int)", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantInListFieldsTest/LoopInvariantInListFieldsTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantInListFieldsTest/LoopInvariantInListFieldsTest.proof index 808669f884c..51939d92614 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantInListFieldsTest/LoopInvariantInListFieldsTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantInListFieldsTest/LoopInvariantInListFieldsTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:21:18 CEST 2016 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=LoopInvariantInListFieldsTest\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "LoopInvariantInListFieldsTest#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNestedListFieldsTest/LoopInvariantNestedListFieldsTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNestedListFieldsTest/LoopInvariantNestedListFieldsTest.proof index b470d648528..558eff78aa7 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNestedListFieldsTest/LoopInvariantNestedListFieldsTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNestedListFieldsTest/LoopInvariantNestedListFieldsTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:21:40 CEST 2016 -name=LoopInvariantNestedListFieldsTest[LoopInvariantNestedListFieldsTest\\:\\:main(LoopInvariantNestedListFieldsTest)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=LoopInvariantNestedListFieldsTest[LoopInvariantNestedListFieldsTest\\:\\:main(LoopInvariantNestedListFieldsTest)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "LoopInvariantNestedListFieldsTest[LoopInvariantNestedListFieldsTest::main(LoopInvariantNestedListFieldsTest)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "LoopInvariantNestedListFieldsTest[LoopInvariantNestedListFieldsTest::main(LoopInvariantNestedListFieldsTest)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNotInListFieldsTest/LoopInvariantNotInListFieldsTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNotInListFieldsTest/LoopInvariantNotInListFieldsTest.proof index 01bb8ec35eb..6a728032079 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNotInListFieldsTest/LoopInvariantNotInListFieldsTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantNotInListFieldsTest/LoopInvariantNotInListFieldsTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:22:07 CEST 2016 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=LoopInvariantNotInListFieldsTest\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "LoopInvariantNotInListFieldsTest#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantStarFieldsTest/LoopInvariantStarFieldsTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantStarFieldsTest/LoopInvariantStarFieldsTest.proof index aac9e88434a..0e1b71de2ff 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantStarFieldsTest/LoopInvariantStarFieldsTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/loopInvariantStarFieldsTest/LoopInvariantStarFieldsTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:22:27 CEST 2016 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=LoopInvariantStarFieldsTest\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "LoopInvariantStarFieldsTest#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodCallTest/MethodCallTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodCallTest/MethodCallTest.proof index f2a79560285..77d6b3bb2ca 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodCallTest/MethodCallTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/methodCallTest/MethodCallTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:22:46 CEST 2016 -name=MethodCallTest[MethodCallTest\\:\\:main(MethodCallTest)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=MethodCallTest[MethodCallTest\\:\\:main(MethodCallTest)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "MethodCallTest[MethodCallTest::main(MethodCallTest)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "MethodCallTest[MethodCallTest::main(MethodCallTest)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 92% 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 a314cb43731..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 14:05:35 CEST 2016 -name=MethodContractAssignableExample[MethodContractAssignableExample\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=MethodContractAssignableExample[MethodContractAssignableExample\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "MethodContractModifiableExample[MethodContractModifiableExample::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "MethodContractModifiableExample[MethodContractModifiableExample::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -79,7 +78,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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")) @@ -90,7 +89,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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 91% 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 18027688b66..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 15:55:42 CEST 2016 -name=MethodContractAssignableLocationNotRequested[MethodContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=MethodContractAssignableLocationNotRequested[MethodContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "MethodContractModifiableLocationNotRequested[MethodContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "MethodContractModifiableLocationNotRequested[MethodContractModifiableLocationNotRequested::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -79,7 +78,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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")) @@ -90,7 +89,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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 91% 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 67204e6e644..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 @@ -41,13 +41,12 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Mar 30 15:53:10 CEST 2016 -name=MethodContractAssignableRequestedLocation[MethodContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=MethodContractAssignableRequestedLocation[MethodContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "MethodContractModifiableRequestedLocation[MethodContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "MethodContractModifiableRequestedLocation[MethodContractModifiableRequestedLocation::main()].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "marti" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) @@ -80,7 +79,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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")) @@ -91,7 +90,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO (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.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceAccess/NestedInstanceAccess.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceAccess/NestedInstanceAccess.proof index 08428502461..a15a516850d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceAccess/NestedInstanceAccess.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceAccess/NestedInstanceAccess.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Feb 02 13:28:41 CET 2015 -name=NestedInstanceAccess[NestedInstanceAccess\\:\\:main(NestedInstanceAccess.A,NestedInstanceAccess.A)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=NestedInstanceAccess[NestedInstanceAccess\\:\\:main(NestedInstanceAccess.A,NestedInstanceAccess.A)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "NestedInstanceAccess[NestedInstanceAccess::main(NestedInstanceAccess.A,NestedInstanceAccess.A)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "NestedInstanceAccess[NestedInstanceAccess::main(NestedInstanceAccess.A,NestedInstanceAccess.A)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceFields/NestedInstanceFields.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceFields/NestedInstanceFields.proof index b0425841e39..c5af37e85f1 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceFields/NestedInstanceFields.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/nestedInstanceFields/NestedInstanceFields.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:23:10 CEST 2016 -name=NestedInstanceFields[NestedInstanceFields\\:\\:main(NestedInstanceFields)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=NestedInstanceFields[NestedInstanceFields\\:\\:main(NestedInstanceFields)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "NestedInstanceFields[NestedInstanceFields::main(NestedInstanceFields)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "NestedInstanceFields[NestedInstanceFields::main(NestedInstanceFields)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/readWriteTest/ReadWriteTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/readWriteTest/ReadWriteTest.proof index 461ed95af0d..4c91922a998 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/readWriteTest/ReadWriteTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/readWriteTest/ReadWriteTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Feb 04 10:23:47 CET 2015 -name=main(int) -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=ReadWriteTest\\#main(int) -"; +\proofObligation { + "name": "main(int)", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "ReadWriteTest#main(int)", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleAliasChanged/SimpleAliasChanged.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleAliasChanged/SimpleAliasChanged.proof index 2a50098640c..f91d89790b4 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleAliasChanged/SimpleAliasChanged.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleAliasChanged/SimpleAliasChanged.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Tue Feb 03 14:53:39 CET 2015 -name=SimpleAliasChanged[SimpleAliasChanged\\:\\:main(SimpleAliasChanged,SimpleAliasChanged)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleAliasChanged[SimpleAliasChanged\\:\\:main(SimpleAliasChanged,SimpleAliasChanged)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleAliasChanged[SimpleAliasChanged::main(SimpleAliasChanged,SimpleAliasChanged)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleAliasChanged[SimpleAliasChanged::main(SimpleAliasChanged,SimpleAliasChanged)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleArrayTest/SimpleArrayTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleArrayTest/SimpleArrayTest.proof index 3bd66f5ea1c..a509d590fcf 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleArrayTest/SimpleArrayTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleArrayTest/SimpleArrayTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:23:31 CEST 2016 -name=SimpleArrayTest[SimpleArrayTest\\:\\:main([I)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleArrayTest[SimpleArrayTest\\:\\:main([I)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleArrayTest[SimpleArrayTest::main([I)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleArrayTest[SimpleArrayTest::main([I)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleInstanceFields/SimpleInstanceFields.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleInstanceFields/SimpleInstanceFields.proof index 2b4c2900c53..bd9a5105e9a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleInstanceFields/SimpleInstanceFields.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleInstanceFields/SimpleInstanceFields.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:23:50 CEST 2016 -name=SimpleInstanceFields[SimpleInstanceFields\\:\\:main(SimpleInstanceFields)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleInstanceFields[SimpleInstanceFields\\:\\:main(SimpleInstanceFields)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleInstanceFields[SimpleInstanceFields::main(SimpleInstanceFields)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleInstanceFields[SimpleInstanceFields::main(SimpleInstanceFields)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLocalVariables/SimpleLocalVariables.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLocalVariables/SimpleLocalVariables.proof index 2e66afadf67..570dbf0c42e 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLocalVariables/SimpleLocalVariables.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLocalVariables/SimpleLocalVariables.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Mar 26 14:14:07 CEST 2018 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=SimpleLocalVariables\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "SimpleLocalVariables#main()", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLoopInvariantTest/SimpleLoopInvariantTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLoopInvariantTest/SimpleLoopInvariantTest.proof index 3c9795e5b57..a9905cbfa91 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLoopInvariantTest/SimpleLoopInvariantTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleLoopInvariantTest/SimpleLoopInvariantTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Feb 18 16:54:18 CET 2015 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=SimpleLoopInvariantTest\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "SimpleLoopInvariantTest#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleMultidimensionArrayTest/SimpleMultidimensionArrayTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleMultidimensionArrayTest/SimpleMultidimensionArrayTest.proof index 650c683a440..5fc8f2aa46d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleMultidimensionArrayTest/SimpleMultidimensionArrayTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleMultidimensionArrayTest/SimpleMultidimensionArrayTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jul 15 10:24:10 CEST 2016 -name=SimpleMultidimensionArrayTest[SimpleMultidimensionArrayTest\\:\\:main([[I)].JML normal_behavior operation contract.0 -addSymbolicExecutionLabel=true -contract=SimpleMultidimensionArrayTest[SimpleMultidimensionArrayTest\\:\\:main([[I)].JML normal_behavior operation contract.0 -addUninterpretedPredicate=true -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "SimpleMultidimensionArrayTest[SimpleMultidimensionArrayTest::main([[I)].JML normal_behavior operation contract.0", + "addSymbolicExecutionLabel": true, + "contract": "SimpleMultidimensionArrayTest[SimpleMultidimensionArrayTest::main([[I)].JML normal_behavior operation contract.0", + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticFields/SimpleStaticFields.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticFields/SimpleStaticFields.proof index 24158603859..f99c36df83d 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticFields/SimpleStaticFields.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticFields/SimpleStaticFields.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Mar 26 14:55:30 CEST 2018 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=SimpleStaticFields\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "SimpleStaticFields#main()", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticLoopInvariantTest/SimpleStatiLoopInvariantTest.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticLoopInvariantTest/SimpleStatiLoopInvariantTest.proof index da924d8337a..f060b77f162 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticLoopInvariantTest/SimpleStatiLoopInvariantTest.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleStaticLoopInvariantTest/SimpleStatiLoopInvariantTest.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Wed Feb 18 16:56:09 CET 2015 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=SimpleStatiLoopInvariantTest\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "SimpleStatiLoopInvariantTest#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleThisInstanceFields/SimpleThisInstanceFields.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleThisInstanceFields/SimpleThisInstanceFields.proof index e6759f9f172..9e9ac8003d6 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleThisInstanceFields/SimpleThisInstanceFields.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/simpleThisInstanceFields/SimpleThisInstanceFields.proof @@ -41,14 +41,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Fri Jan 30 14:53:56 CET 2015 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=SimpleThisInstanceFields\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "SimpleThisInstanceFields#main()", + } \proof { (keyLog "0" (keyUser "Martin" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/valueChange/ValueChange.proof b/key.core.symbolic_execution/src/test/resources/testcase/slicing/valueChange/ValueChange.proof index 0950c31ad5d..8925596df5a 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/valueChange/ValueChange.proof +++ b/key.core.symbolic_execution/src/test/resources/testcase/slicing/valueChange/ValueChange.proof @@ -43,14 +43,13 @@ \javaSource ""; -\proofObligation "#Proof Obligation Settings -#Mon Mar 26 14:38:35 CEST 2018 -name=main() -addSymbolicExecutionLabel=true -addUninterpretedPredicate=true -class=de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO -method=ValueChange\\#main() -"; +\proofObligation { + "name": "main()", + "addSymbolicExecutionLabel": true, + "addUninterpretedPredicate": true, + "class": "de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO", + "method": "ValueChange#main()", + } \proof { (keyLog "0" (keyUser "bubel" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java index 96d99994211..00f24ad3c1f 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java @@ -296,8 +296,7 @@ public void set(TestGenerationSettings settings) { } - @Nullable - private static TestGenerationSettings instance; + private static @Nullable TestGenerationSettings instance; public static @NonNull TestGenerationSettings getInstance() { if (instance == null) { 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.testgen/src/test/resources/testcase/smt/ce/middle.key b/key.core.testgen/src/test/resources/testcase/smt/ce/middle.key index 5c8f265c960..6a8593b88e4 100644 --- a/key.core.testgen/src/test/resources/testcase/smt/ce/middle.key +++ b/key.core.testgen/src/test/resources/testcase/smt/ce/middle.key @@ -40,12 +40,11 @@ \javaSource "src"; -\proofObligation "#Proof Obligation Settings -#Fri Jun 06 15:00:21 CEST 2014 -name=Middle[Middle\\:\\:middle(int,int,int)].JML normal_behavior operation contract.0 -contract=Middle[Middle\\:\\:middle(int,int,int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "Middle[Middle::middle(int,int,int)].JML normal_behavior operation contract.0", + "contract": "Middle[Middle::middle(int,int,int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "mihai" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) diff --git a/key.core.testgen/src/test/resources/testcase/smt/tg/middle.key b/key.core.testgen/src/test/resources/testcase/smt/tg/middle.key index 5c8f265c960..6a8593b88e4 100644 --- a/key.core.testgen/src/test/resources/testcase/smt/tg/middle.key +++ b/key.core.testgen/src/test/resources/testcase/smt/tg/middle.key @@ -40,12 +40,11 @@ \javaSource "src"; -\proofObligation "#Proof Obligation Settings -#Fri Jun 06 15:00:21 CEST 2014 -name=Middle[Middle\\:\\:middle(int,int,int)].JML normal_behavior operation contract.0 -contract=Middle[Middle\\:\\:middle(int,int,int)].JML normal_behavior operation contract.0 -class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO -"; +\proofObligation { + "name": "Middle[Middle::middle(int,int,int)].JML normal_behavior operation contract.0", + "contract": "Middle[Middle::middle(int,int,int)].JML normal_behavior operation contract.0", + "class": "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + } \proof { (keyLog "0" (keyUser "mihai" ) (keyVersion "90bb886cd7b78027c8f6703803461f09e5699bb9")) 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 788187f9849..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,8 +356,7 @@ jmlprimary | VALUES #primaryValues | STRING_EQUAL LPAREN expression COMMA expression RPAREN #primaryStringEq | EMPTYSET #primaryEmptySet - | STOREREF LPAREN storeRefUnion RPAREN #primaryStoreRef - | LOCSET LPAREN fieldarrayaccess (COMMA fieldarrayaccess)* RPAREN #primaryCreateLocset + | (LOCSET|STOREREF) LPAREN storeRefUnion? RPAREN #primaryStoreRef | SINGLETON LPAREN expression RPAREN #primaryCreateLocsetSingleton | UNION LPAREN storeRefUnion RPAREN #primaryUnion | INTERSECT LPAREN storeRefIntersect RPAREN #primaryIntersect @@ -363,18 +371,10 @@ jmlprimary | sequence #primaryignore10 ; -fieldarrayaccess: (ident|this_|super_) (fieldarrayaccess_suffix)*; -fieldarrayaccess_suffix - : DOT (ident | inv | inv_free | this_ | super_ | TRANSIENT | INV | INV_FREE) - | LBRACKET (expression) RBRACKET -; - -super_: SUPER; - 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 1ef3866446a..33c7977ff9a 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'; @@ -529,4 +529,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 2a2926ea015..733c83f6882 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -39,7 +39,7 @@ problem : ( PROBLEM LBRACE ( t=termorseq ) RBRACE | CHOOSECONTRACT (chooseContract=string_value SEMI)? - | PROOFOBLIGATION (proofObligation=string_value SEMI)? + | PROOFOBLIGATION (proofObligation=cvalue)? SEMI? ) proofScript? ; @@ -804,7 +804,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/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java index 5482648451f..511292f6103 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java @@ -302,7 +302,7 @@ private Term addOrigin(Term term) { private ProgramElement parseRow(int irow) throws SVInstantiationParserException { String instantiation = (String) getValueAt(irow, 1); - SchemaVariable sv = (SchemaVariable) getValueAt(irow, 0); + ProgramSV sv = (ProgramSV) getValueAt(irow, 0); ContextInstantiationEntry contextInstantiation = originalApp.instantiations().getContextInstantiation(); @@ -353,7 +353,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException { sort = idd.sort(); if (sort == null) { try { - sort = result.getRealSort(sv, services); + sort = result.getRealSort((OperatorSV) sv, services); } catch (SortException e) { throw new MissingSortException(String.valueOf(sv), createPosition(irow)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java index a7b80f23363..31af38cee26 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java @@ -24,7 +24,7 @@ import org.key_project.util.collection.ImmutableList; -import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; /** @@ -55,7 +55,7 @@ public String getDescription() { @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - if (goals == null || goals.head() == null || goals.head().node() == null + if (goals == null || goals.isEmpty() || goals.head().node() == null || goals.head().node().parent() == null) { return false; } @@ -80,7 +80,7 @@ public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrenc final Term selfComposedExec = f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION); - return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY); + return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java index cd9f38083b4..ebc09fb6764 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java @@ -25,7 +25,7 @@ import org.key_project.util.collection.ImmutableList; -import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; public class StartAuxiliaryLoopComputationMacro extends AbstractProofMacro implements StartSideProofMacro { @@ -51,7 +51,7 @@ public String getDescription() { @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - if (goals == null || goals.head() == null || goals.head().node() == null + if (goals == null || goals.isEmpty() || goals.head().node() == null || goals.head().node().parent() == null) { return false; } @@ -77,7 +77,7 @@ public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrenc final Term selfComposedExec = f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_LOOP_WITH_INV_RELATION); - return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY); + return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java index 33dc44f19d0..c50dc66610e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java @@ -22,7 +22,7 @@ import org.key_project.util.collection.ImmutableList; -import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; /** * @@ -52,7 +52,7 @@ public String getDescription() { @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - if (goals == null || goals.head() == null) { + if (goals == null || goals.isEmpty()) { return false; } if (posInOcc == null || posInOcc.subTerm() == null) { @@ -69,7 +69,7 @@ public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrenc final Term selfComposedExec = f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_EXECUTION_WITH_PRE_RELATION); - return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY); + return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java index 89f769146f5..6c48fe9b0b6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java @@ -5,7 +5,6 @@ import java.util.List; import java.util.Map; -import java.util.Properties; import de.uka.ilkd.key.informationflow.po.snippet.BasicPOSnippetFactory; import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory; @@ -21,6 +20,7 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.*; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.speclang.BlockContract; import de.uka.ilkd.key.speclang.ContractFactory; @@ -166,11 +166,14 @@ public ExecutionContext getExecutionContext() { /** * {@inheritDoc} + * + * @return */ @Override - public void fillSaveProperties(Properties properties) { - super.fillSaveProperties(properties); - properties.setProperty("Non-interference contract", contract.getUniqueName()); + public Configuration createLoaderConfig() { + var c = super.createLoaderConfig(); + c.set("Non-interference contract", contract.getUniqueName()); + return c; } @Override @@ -249,8 +252,8 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -259,9 +262,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -271,7 +274,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @@ -279,8 +283,8 @@ protected Term buildFrameClause(List modHeaps, Map @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java index 217093da97a..dc0912874df 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java @@ -66,7 +66,12 @@ private void linkSymbExecVarsToCopies() { private void linkStateVarsToCopies(StateVars ifVars, StateVars seVars, Map map) { final Iterator ifVarsIt = ifVars.termList.iterator(); for (final Term symbTerm : seVars.termList) { - final Term ifTerm = ifVarsIt.next(); + final Term ifTerm; + if (ifVarsIt.hasNext()) { + ifTerm = ifVarsIt.next(); + } else { + ifTerm = null; + } if (symbTerm != null) { map.put(symbTerm, ifTerm); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java index d531f2271bc..1b1dd411a00 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java @@ -5,7 +5,6 @@ import java.util.List; import java.util.Map; -import java.util.Properties; import de.uka.ilkd.key.informationflow.po.snippet.InfFlowPOSnippetFactory; import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory; @@ -19,7 +18,7 @@ import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.proof.init.*; import de.uka.ilkd.key.rule.NoPosTacletApp; -import de.uka.ilkd.key.speclang.Contract; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.speclang.InformationFlowContract; import org.key_project.logic.Named; @@ -171,30 +170,14 @@ public IFProofObligationVars getIFVars() { /** * {@inheritDoc} - */ - @Override - public void fillSaveProperties(Properties properties) { - super.fillSaveProperties(properties); - properties.setProperty("contract", contract.getName()); - } - - - /** - * Instantiates a new proof obligation with the given settings. * - * @param initConfig The already load {@link InitConfig}. - * @param properties The settings of the proof obligation to instantiate. - * @return The instantiated proof obligation. + * @return */ - public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) { - final String contractName = properties.getProperty("contract"); - final Contract contract = - initConfig.getServices().getSpecificationRepository().getContractByName(contractName); - if (contract == null) { - throw new RuntimeException("Contract not found: " + contractName); - } else { - return new LoadedPOContainer(contract.createProofObl(initConfig), 0); - } + @Override + public Configuration createLoaderConfig() { + var c = super.createLoaderConfig(); + c.set("contract", contract.getName()); + return c; } @@ -261,8 +244,8 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -271,9 +254,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -283,7 +266,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @@ -291,8 +275,8 @@ protected Term buildFrameClause(List modHeaps, Map @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPOLoader.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPOLoader.java new file mode 100644 index 00000000000..63fedab22bd --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPOLoader.java @@ -0,0 +1,49 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.informationflow.po; + +import de.uka.ilkd.key.proof.init.IPersistablePO; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.init.loader.ProofObligationLoader; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.speclang.Contract; + +import org.jspecify.annotations.NullMarked; + +/** + * Loader for information flow proof obligations. + * + * @author Alexander Weigl + * @version 1 (28.12.23) + */ +@NullMarked +public class InfFlowContractPOLoader implements ProofObligationLoader { + + /** + * Instantiates a new proof obligation with the given settings. + * + * @param initConfig The already loaded {@link InitConfig}. + * @param properties The settings of the proof obligation to instantiate. + * @return The instantiated proof obligation. + */ + public IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, + Configuration properties) { + final String contractName = properties.getString("contract"); + final Contract contract = + initConfig.getServices().getSpecificationRepository().getContractByName(contractName); + if (contract == null) { + throw new RuntimeException("Contract not found: " + contractName); + } else { + return new IPersistablePO.LoadedPOContainer(contract.createProofObl(initConfig), 0); + } + } + + @Override + public boolean handles(String identifier) { + return InfFlowContractPO.class.getName().equals(identifier) + || InfFlowContractPO.class.getSimpleName().equals(identifier) + || InfFlowContractPOLoader.class.getName().equals(identifier) + || InfFlowContractPOLoader.class.getSimpleName().equals(identifier); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java index 4a587dc9311..d3fa706086b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java @@ -613,11 +613,13 @@ private void printSchemaVariables(StringBuilder result) { result.append("\\schemaVariables{\n"); for (final SchemaVariable sv : getSchemaVariables()) { - final String prefix = sv instanceof FormulaSV ? "\\formula " - : sv instanceof TermSV ? "\\term " : "\\variables "; + if (!(sv instanceof OperatorSV asv)) + continue; + final String prefix = asv instanceof FormulaSV ? "\\formula " + : asv instanceof TermSV ? "\\term " : "\\variables "; result.append(prefix); - result.append(sv.sort().name()).append(" "); - result.append(sv.name()); + result.append(asv.sort().name()).append(" "); + result.append(asv.name()); result.append(";\n"); } result.append("}\n\n"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java index 30a1e893a65..172c30a38af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java @@ -5,7 +5,6 @@ import java.util.List; import java.util.Map; -import java.util.Properties; import de.uka.ilkd.key.informationflow.po.snippet.BasicPOSnippetFactory; import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory; @@ -21,6 +20,7 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.*; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.speclang.ContractFactory; import de.uka.ilkd.key.speclang.LoopSpecification; import de.uka.ilkd.key.util.InfFlowSpec; @@ -167,11 +167,14 @@ protected String buildPOName(boolean transactionFlag) { /** * {@inheritDoc} + * + * @return */ @Override - public void fillSaveProperties(Properties properties) { - super.fillSaveProperties(properties); - properties.setProperty("Non-interference contract", loopInvariant.getUniqueName()); + public Configuration createLoaderConfig() { + var c = super.createLoaderConfig(); + c.set("Non-interference contract", loopInvariant.getUniqueName()); + return c; } @@ -250,16 +253,16 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -267,9 +270,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -278,7 +281,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java index 9432fcae9c8..d82be5eb93c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java @@ -5,7 +5,6 @@ import java.util.List; import java.util.Map; -import java.util.Properties; import de.uka.ilkd.key.informationflow.po.snippet.BasicPOSnippetFactory; import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory; @@ -20,6 +19,7 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.*; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.speclang.ContractFactory; import de.uka.ilkd.key.speclang.InformationFlowContract; @@ -170,11 +170,14 @@ public Goal getInitiatingGoal() { /** * {@inheritDoc} + * + * @return */ @Override - public void fillSaveProperties(Properties properties) { - super.fillSaveProperties(properties); - properties.setProperty("Non-interference contract", contract.getName()); + public Configuration createLoaderConfig() { + var c = super.createLoaderConfig(); + c.set("Non-interference contract", contract.getName()); + return c; } @Override @@ -253,8 +256,8 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -263,9 +266,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -275,7 +278,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @@ -283,8 +287,8 @@ protected Term buildFrameClause(List modHeaps, Map @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } 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 320f8b6aa96..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 @@ -15,6 +15,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.IObserverFunction; +import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.Modality; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.speclang.*; @@ -89,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 @@ -124,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()); @@ -144,27 +145,27 @@ 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 = + final ImmutableSet localInVariables = MiscTools.getLocalIns(invariant.getLoop(), services); - final ImmutableSet localOutVariables = + final ImmutableSet localOutVariables = MiscTools.getLocalOuts(invariant.getLoop(), services); final ImmutableList localInTerms = toTermList(localInVariables); final ImmutableList localOutTerms = toTermList(localOutVariables); @@ -186,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()); @@ -210,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