diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index a13aecf615f..327890ba723 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -20,7 +20,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Build with Gradle run: ./gradlew -DENABLE_NULLNESS=true compileTest @@ -49,7 +49,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: SpotlessCheck run: ./gradlew --continue spotlessCheck @@ -81,7 +81,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Checkstyle run: ./gradlew --continue checkstyleMainChanged - run: | @@ -108,7 +108,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: PMD checks run: ./gradlew --continue pmdMainChanged diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml index e46dd959484..ab43091e529 100644 --- a/.github/workflows/gradle-publish.yml +++ b/.github/workflows/gradle-publish.yml @@ -22,7 +22,7 @@ jobs: server-id: github # Value of the distributionManagement/repository/id field of the pom.xml - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Assemble with Gradle run: ./gradlew assemble diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index 82e5a48f7be..1ebbb82c9fe 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -19,7 +19,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Build Documentation with Gradle run: ./gradlew alldoc diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 97cd713ffac..f60a7fc2762 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -31,7 +31,7 @@ jobs: distribution: 'temurin' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Build with Gradle run: ./gradlew --parallel assemble diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 360cb718d81..8093ed2b328 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -25,7 +25,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Test with Gradle run: ./gradlew --continue ${{ matrix.tests }} diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index a9f68ed0541..e45ebec48c2 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -38,7 +38,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Test with Gradle run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -87,7 +87,7 @@ jobs: shell: bash - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml index 96a248d0b2c..fd4cbb74b31 100644 --- a/.github/workflows/tests_winmac.yml +++ b/.github/workflows/tests_winmac.yml @@ -30,7 +30,7 @@ jobs: - name: Setup Gradle uses: - gradle/actions/setup-gradle@v3.3.2 + gradle/actions/setup-gradle@v3.4.2 - name: Test with Gradle run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -76,7 +76,7 @@ jobs: run: .github/dlsmt.sh - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} diff --git a/build.gradle b/build.gradle index 935addaa9a8..6df46bffc01 100644 --- a/build.gradle +++ b/build.gradle @@ -24,7 +24,7 @@ plugins { id "com.diffplug.spotless" version "6.25.0" // EISOP Checker Framework - id "org.checkerframework" version "0.6.39" + id "org.checkerframework" version "0.6.41" } // Configure this project for use inside IntelliJ: @@ -90,11 +90,11 @@ subprojects { checkerFramework "io.github.eisop:checker:$eisop_version" testImplementation("ch.qos.logback:logback-classic:1.5.6") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2' + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3' testImplementation project(':key.util') - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2' + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.3' } tasks.withType(JavaCompile) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 9bfd785e9e4..82ee5ef01ad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -209,7 +209,13 @@ public void save(OutputStream out) throws IOException { } final Sequent problemSeq = proof.root().sequent(); ps.println("\\problem {"); - printer.printSemisequent(problemSeq.succedent()); + if (problemSeq.antecedent().isEmpty() && problemSeq.succedent().size() == 1) { + // Problem statement is a single formula ... + printer.printSemisequent(problemSeq.succedent()); + } else { + // Problem statement is a proper sequent ... + printer.printSequent(problemSeq); + } ps.println(printer.result()); ps.println("}\n"); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java new file mode 100644 index 00000000000..d55f9f78743 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java @@ -0,0 +1,54 @@ +/* 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.proof.io; + +import java.io.File; +import java.io.IOException; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.nparser.KeyIO; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.init.AbstractProfile; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.rule.TacletForTests; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +class ProofSaverTest { + + void testSaveProblemToFile(String content) throws IOException { + Services services = TacletForTests.services(); + KeyIO io = new KeyIO(services); + KeyIO.Loader loader = io.load(content); + Sequent seq = loader.parseFile().loadProblem().getProblem(); + final InitConfig initConfig = + new InitConfig(new Services(AbstractProfile.getDefaultProfile())); + Proof proof = new Proof("test", seq, "", initConfig, null); + File file = File.createTempFile("proofSaveTest", ".key"); + file.deleteOnExit(); + String status = new ProofSaver(proof, file).save(); + assertNull(status); + + KeyIO io2 = new KeyIO(services); + KeyIO.Loader loader2 = io2.load(content); + Sequent seq2 = loader2.parseFile().loadProblem().getProblem(); + + assertEquals(seq, seq2); + } + + @Test + void saveTermProblemToFile() throws IOException { + String content = "\\problem { true }"; + testSaveProblemToFile(content); + } + + @Test + void saveSequentProblemToFile() throws IOException { + String content = "\\problem { true, false ==> false, false }"; + testSaveProblemToFile(content); + } +}