diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index c962aa4a212..256132a6171 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -22,7 +22,7 @@ jobs: - name: Setup Gradle uses: gradle/actions/setup-gradle@v5 - name: Build with Gradle - run: ./gradlew -DENABLE_NULLNESS=true compileTest + run: ./gradlew -DENABLE_NULLNESS=true compileTestJava formatting: runs-on: ubuntu-latest diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index c8523b23afc..60998a055c9 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -28,7 +28,8 @@ jobs: modules: [ keyext.exploration, keyext.slicing, key.ncore, key.ui, key.core, key.core.testgen, keyext.isabelletranslation, keyext.ui.testgen, key.ncore.calculus, - key.util, key.core.example, keyext.caching, keyext.proofmanagement] + key.util, key.core.example, keyext.caching, key.core.wd, key.core.infflow, + keyext.proofmanagement] continue-on-error: true runs-on: ${{ matrix.os }} env: diff --git a/build.gradle b/build.gradle index 2ea8d7a2ffa..913da9b90c2 100644 --- a/build.gradle +++ b/build.gradle @@ -83,18 +83,17 @@ subprojects { testImplementation("ch.qos.logback:logback-classic:1.5.32") testImplementation(platform("org.junit:junit-bom:5.14.3")) - testImplementation ("org.junit.jupiter:junit-jupiter-api") - testImplementation ("org.junit.jupiter:junit-jupiter-params") - testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine") - testRuntimeOnly ("org.junit.platform:junit-platform-launcher") - testImplementation ("org.assertj:assertj-core:3.27.7") - testImplementation project(':key.util') + testImplementation("org.junit.jupiter:junit-jupiter-api") + testImplementation("org.junit.jupiter:junit-jupiter-params") + testRuntimeOnly("org.junit.jupiter:junit-jupiter-engine") + testRuntimeOnly("org.junit.platform:junit-platform-launcher") + testImplementation("org.assertj:assertj-core:3.27.7") + testImplementation(project(':key.util')) + testImplementation(testFixtures(project(":key.util"))) // test fixtures testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.1") testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.21.1") - - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine' } tasks.withType(JavaCompile).configureEach { diff --git a/key.core.example/src/main/resources/logback.xml b/key.core.example/src/main/resources/logback.xml deleted file mode 100644 index de2952bde1c..00000000000 --- a/key.core.example/src/main/resources/logback.xml +++ /dev/null @@ -1,56 +0,0 @@ - - - - - - - - ${user.home}/.key/logs/key_${timestamp}.log - false - - UTF-8 - - %date|%level|%thread|%logger|%file:%line|%replace(%msg){'[\n\r]','\\n'}|%replace(%ex){'[\n\r]','\\n'}%nopex|%n - true - - - - - - [%date{HH:mm:ss.SSS}] %highlight(%-5level) %cyan(%logger{0}) - %msg%ex%n - - - - INFO - - - - - - - - - - - - [%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n - - - TRACE - - - - - - - diff --git a/key.core.infflow/build.gradle b/key.core.infflow/build.gradle index 127fb89f356..208feccfd64 100644 --- a/key.core.infflow/build.gradle +++ b/key.core.infflow/build.gradle @@ -2,7 +2,8 @@ dependencies { api(project(":key.core")) - testImplementation(project(":key.core").sourceSets.test.output) + + testImplementation(testFixtures(project(":key.core"))) } diff --git a/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java index 42c0bfe73ef..ea0106313bd 100644 --- a/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java +++ b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java @@ -7,12 +7,10 @@ import java.nio.file.Paths; import java.util.*; -import de.uka.ilkd.key.proof.runallproofs.ProofCollections; - import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import static de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests.*; +import static de.uka.ilkd.key.proof.runallproofs.GenerateUnitTestsUtil.*; /** * Generation of test cases (JUnit) for given proof collection files. @@ -21,7 +19,7 @@ * {@code generateRunAllProofs}. *

* The considered proof collections files are configured statically in - * {@link ProofCollections}. + * {@link InfFlowProofCollection}. * * @author Alexander Weigl * @version 1 (6/14/20) diff --git a/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/InfFlowTests.java b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/InfFlowTests.java new file mode 100644 index 00000000000..566f0d9a6c3 --- /dev/null +++ b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/InfFlowTests.java @@ -0,0 +1,17 @@ +/* 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; + +import org.junit.jupiter.api.Test; + +/** + * + * @author Alexander Weigl + * @version 1 (2/20/26) + */ +public class InfFlowTests { + // Empty test to trick or non-empty test case requirements. + @Test + public void testInfFlowEmpty() {} +} diff --git a/key.core.proof_references/src/test/resources/logback.xml b/key.core.proof_references/src/test/resources/logback.xml deleted file mode 100644 index 13617d11a78..00000000000 --- a/key.core.proof_references/src/test/resources/logback.xml +++ /dev/null @@ -1,14 +0,0 @@ - - - - key.log - false - - %-10relative %-5level %-15thread %-25logger{5} %msg %ex{long}%n - - - - - - - \ No newline at end of file diff --git a/key.core.symbolic_execution/build.gradle b/key.core.symbolic_execution/build.gradle index 697c8045706..42d92ad7f6c 100644 --- a/key.core.symbolic_execution/build.gradle +++ b/key.core.symbolic_execution/build.gradle @@ -2,7 +2,6 @@ description = "API for using KeY as a symbolic execution engine for Java program dependencies { implementation project(":key.core") - testImplementation project(":key.core").sourceSets.test.output } test { diff --git a/key.core.symbolic_execution/src/test/resources/logback.xml b/key.core.symbolic_execution/src/test/resources/logback.xml deleted file mode 100644 index 093c00426b0..00000000000 --- a/key.core.symbolic_execution/src/test/resources/logback.xml +++ /dev/null @@ -1,16 +0,0 @@ - - - - - - key.log - false - - %-10relative %-5level %-15thread %-25logger{5} %msg %ex{long}%n - - - - - - - \ No newline at end of file diff --git a/key.core.testgen/src/test/resources/logback.xml b/key.core.testgen/src/test/resources/logback.xml deleted file mode 100644 index 6275136f42e..00000000000 --- a/key.core.testgen/src/test/resources/logback.xml +++ /dev/null @@ -1,13 +0,0 @@ - - - key.log - false - - %-10relative %-5level %-15thread %-25logger{5} %msg %ex{long}%n - - - - - - - \ No newline at end of file diff --git a/key.core.wd/build.gradle b/key.core.wd/build.gradle index 6db19fa7ebf..ccf546b22cc 100644 --- a/key.core.wd/build.gradle +++ b/key.core.wd/build.gradle @@ -1,6 +1,7 @@ dependencies { api(project(":key.core")) - testImplementation(project(":key.core").sourceSets.test.output) + + testImplementation(testFixtures(project(":key.core"))) } tasks.register('testRunAllWdProofs', Test) { diff --git a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java index fa607a3ccce..592df6437bc 100644 --- a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java +++ b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java @@ -7,13 +7,11 @@ import java.nio.file.Paths; import java.util.List; -import de.uka.ilkd.key.proof.runallproofs.ProofCollections; +import de.uka.ilkd.key.proof.runallproofs.GenerateUnitTestsUtil; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import static de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests.*; - /** * Generation of test cases (JUnit) for given proof collection files. *

@@ -36,6 +34,6 @@ public static void main(String[] args) throws IOException { System.exit(1); } var outputFolder = Paths.get(args[0]); - run(outputFolder, collections); + GenerateUnitTestsUtil.run(outputFolder, collections); } } diff --git a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java index c59302fea3f..2b1c83ef459 100644 --- a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java +++ b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection; import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings; -import static de.uka.ilkd.key.proof.runallproofs.ProofCollections.loadFromFile; +import static de.uka.ilkd.key.proof.runallproofs.GenerateUnitTestsUtil.loadFromFile; import static org.assertj.core.api.Assertions.assertThat; public class WdProofCollection { @@ -147,10 +147,10 @@ public static ProofCollection automaticWd() throws IOException { g.provable("./firstTouch/10-SITA/SITA3_rearrangeWithWDLoop.key"); g.provable("./firstTouch/10-SITA/SITA3_swapWD.key"); - g = c.group("wd_blockcontracts"); + // g = c.group("wd_blockcontracts"); // g.notprovable("./heap/block_contracts/GreatestCommonDivisor_ofWithWD.key"); - g = c.group("wd_fm12_01_LRS"); + // g = c.group("wd_fm12_01_LRS"); // g.notprovable("./heap/fm12_01_LRS/LCP_lcpWD.key"); // g.notprovable("./heap/fm12_01_LRS/LRS_doLRSWD.key"); // g.notprovable("./heap/fm12_01_LRS/SuffixArray_invariantWD.key"); diff --git a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdTests.java b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdTests.java new file mode 100644 index 00000000000..437b26a70c1 --- /dev/null +++ b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdTests.java @@ -0,0 +1,17 @@ +/* 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.wd; + +import org.junit.jupiter.api.Test; + +/** + * + * @author Alexander Weigl + * @version 1 (2/20/26) + */ +public class WdTests { + // Empty test to trick or non-empty test case requirements. + @Test + public void testInfFlowEmpty() {} +} diff --git a/key.core/build.gradle b/key.core/build.gradle index 69a6d954e8e..7d4e9da7509 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -1,4 +1,5 @@ plugins { + id 'java-test-fixtures' } description = "Core functionality (terms, rules, prover, ...) for deductive verification of Java programs" @@ -9,16 +10,11 @@ dependencies { api project(':key.util') api project(':key.ncore') api project(':key.ncore.calculus') - testImplementation 'junit:junit:4.13.1' - //api group: group, name: 'recoderkey', version: '1.0' - - // JavaCC - //implementation group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' - //javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' antlr4 "org.antlr:antlr4:4.13.2" api "org.antlr:antlr4-runtime:4.13.2" + api project(':key.util') def JP_VERSION = "3.28.0-K13.5" @@ -31,6 +27,9 @@ dependencies { // https://mvnrepository.com/artifact/com.fasterxml.jackson.dataformat/jackson-dataformat-yaml testImplementation 'com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.15.2' + + // test fixtures + testFixturesApi(testFixtures(project(":key.util"))) } // The target directory for JavaCC (parser generation) diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index 19491d1632d..8c89b56d83b 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -11,10 +11,6 @@ import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection; import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings; -import org.key_project.util.java.IOUtil; - -import org.junit.jupiter.api.Assertions; - /** * This class configuress the "runAllProofs" test runs. * @@ -108,7 +104,7 @@ public static ProofCollection automaticJavaDL() throws IOException { // runOnlyOn = group1, group2 (the space after each comma is mandatory) // settings.setRunOnlyOn("performance, performancePOConstruction"); - settings.setKeySettings(loadFromFile("automaticJAVADL.properties")); + settings.setKeySettings(GenerateUnitTestsUtil.loadFromFile("automaticJAVADL.properties")); var c = new ProofCollection(settings); @@ -1026,12 +1022,4 @@ public static ProofCollection automaticJavaDL() throws IOException { } return c; } - - - public static String loadFromFile(String name) throws IOException { - var stream = ProofCollections.class.getResourceAsStream(name); - Assertions.assertNotNull(stream, "Failed to find " + name); - return IOUtil.readFrom(stream); - } - } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RunAllProofsTestWithComputeCostProfiling.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestWithComputeCostProfiling.java similarity index 93% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RunAllProofsTestWithComputeCostProfiling.java rename to key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestWithComputeCostProfiling.java index 030baf7de9a..b5eec32dc8d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RunAllProofsTestWithComputeCostProfiling.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestWithComputeCostProfiling.java @@ -1,7 +1,7 @@ /* 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.runallproofs.performance; +package de.uka.ilkd.key.proof.runallproofs; import java.io.File; import java.io.IOException; @@ -9,9 +9,7 @@ import java.util.Objects; import java.util.stream.Stream; -import de.uka.ilkd.key.proof.runallproofs.ProofCollections; -import de.uka.ilkd.key.proof.runallproofs.RunAllProofsFunctional; -import de.uka.ilkd.key.proof.runallproofs.RunAllProofsTest; +import de.uka.ilkd.key.proof.runallproofs.performance.ProfilingDirectories; import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection; import org.key_project.prover.rules.RuleApp; diff --git a/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTestsUtil.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTestsUtil.java new file mode 100644 index 00000000000..b2115223d65 --- /dev/null +++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTestsUtil.java @@ -0,0 +1,186 @@ +/* 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.runallproofs; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection; +import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings; +import de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile; + +import org.key_project.util.java.IOUtil; + +import org.junit.jupiter.api.Assertions; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Generation of test cases (JUnit) for given proof collection files. + *

+ * This class is intended to be called from gradle. See the gradle task + * {@code generateRunAllProofs}. + *

+ * The considered proof collections files are configured statically in the source code. + * + * @author Alexander Weigl + * @version 1 (6/14/20) + */ +public class GenerateUnitTestsUtil { + private static final Logger LOGGER = LoggerFactory.getLogger(GenerateUnitTestsUtil.class); + + public static void run(Path outputFolder, List collections) + throws IOException { + LOGGER.info("Output folder {}", outputFolder); + + outputFolder = outputFolder.toAbsolutePath(); + Files.createDirectories(outputFolder); + + for (var col : collections) { + for (RunAllProofsTestUnit unit : col.createRunAllProofsTestUnits()) { + createUnitClass(outputFolder, unit); + } + } + } + + private static final String TEMPLATE_CONTENT = + """ + /* 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 $packageName; + + import org.junit.jupiter.api.*; + import static org.junit.jupiter.api.Assertions.*; + + public class $className extends de.uka.ilkd.key.proof.runallproofs.ProveTest { + public static final String STATISTIC_FILE = "$statisticsFile"; + + { // initialize during construction + this.baseDirectory = "$baseDirectory"; + this.statisticsFile = STATISTIC_FILE; + this.name = "$name"; + this.reloadEnabled = $reloadEnabled; + this.tempDir = "$tempDir"; + + this.globalSettings = "$keySettings"; + this.localSettings = "$localSettings"; + } + + $timeout + $methods + } + """; + + /** + * Generates the test classes for the given proof collection, and writes the + * java files. + * + * @param unit a group of proof collection units + * @throws IOException if the file is not writable + */ + private static void createUnitClass(Path outputFolder, RunAllProofsTestUnit unit) + throws IOException { + String packageName = "de.uka.ilkd.key.proof.runallproofs.gen"; + String name = unit.getTestName(); + String className = '_' + name // avoids name clashes, i.e., group "switch" + .replaceAll("\\.java", "") + .replaceAll("\\.key", "") + .replaceAll("[^a-zA-Z0-9]+", "_"); + + ProofCollectionSettings settings = unit.getSettings(); + Map vars = new TreeMap<>(); + vars.put("className", className); + vars.put("packageName", packageName); + vars.put("baseDirectory", settings.getBaseDirectory().getAbsolutePath() + .replaceAll("\\\\", "/")); + vars.put("statisticsFile", + settings.getStatisticsFile().getStatisticsFile().getAbsolutePath() + .replaceAll("\\\\", "/")); + vars.put("name", name); + vars.put("reloadEnabled", String.valueOf(settings.reloadEnabled())); + vars.put("tempDir", settings.getTempDir().getAbsolutePath() + .replaceAll("\\\\", "/")); + + vars.put("globalSettings", settings.getGlobalKeYSettings().replace("\n", "\\n")); + vars.put("localSettings", + (settings.getLocalKeYSettings() == null ? "" : settings.getLocalKeYSettings()) + .replace("\n", "\\n")); + + vars.put("timeout", ""); + + if (false) {// disabled + int globalTimeout = 0; + if (globalTimeout > 0) { + vars.put("timeout", + "@Rule public Timeout globalTimeout = Timeout.seconds(" + globalTimeout + ");"); + } + } + + StringBuilder methods = new StringBuilder(); + Set usedMethodNames = new TreeSet<>(); + int clashCounter = 0; + + for (TestFile file : unit.getTestFiles()) { + Path keyFile = file.getKeYFile(); + String testName = keyFile.getFileName().toString() + .replaceAll("\\.java", "") + .replaceAll("\\.key", "") + .replaceAll("[^a-zA-Z0-9]+", "_"); + + if (usedMethodNames.contains(testName)) { + testName += "_" + (++clashCounter); + } + usedMethodNames.add(testName); + + // int timeout = 0; (timeout <= 0 ? parent.timeout : 0) + String to = ""; // timeout > 0 ? "timeout=${1000 * timeout}" : ""; + methods.append("\n"); + methods.append("@Test(").append(to).append(")") + // .append("@TestName(\"").append(keyFile.getName()).append("\")") + .append("void test").append(testName).append("() throws Exception {\n"); + // "// This tests is based on").append(keyFile.toAbsolutePath()).append("\n"); + + switch (file.getTestProperty()) { + case PROVABLE -> methods.append("assertProvability(\"") + .append(keyFile.toAbsolutePath().toString().replaceAll("\\\\", "/")) + .append("\");"); + case NOTPROVABLE -> methods.append("assertUnProvability(\"") + .append(keyFile.toAbsolutePath().toString().replaceAll("\\\\", "/")) + .append("\");"); + case LOADABLE -> methods.append("assertLoadability(\"") + .append(keyFile.toAbsolutePath().toString().replaceAll("\\\\", "/")) + .append("\");"); + case NOTLOADABLE -> methods.append("assertUnLoadability(\"") + .append(keyFile.toAbsolutePath().toString().replaceAll("\\\\", "/")) + .append("\");"); + } + methods.append("}"); + } + vars.put("methods", methods.toString()); + + Pattern regex = Pattern.compile("[$](\\w+)"); + Matcher m = regex.matcher(TEMPLATE_CONTENT); + StringBuilder sb = new StringBuilder(); + while (m.find()) { + String key = m.group(1); + m.appendReplacement(sb, vars.getOrDefault(key, "/*not-found*/")); + } + m.appendTail(sb); + var folder = outputFolder.resolve(packageName.replace('.', '/')); + Files.createDirectories(folder); + Files.writeString(folder.resolve(className + ".java"), sb.toString()); + } + + public static String loadFromFile(String name) throws IOException { + var stream = GenerateUnitTestsUtil.class.getResourceAsStream(name); + Assertions.assertNotNull(stream, "Failed to find " + name); + return IOUtil.readFrom(stream); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/JunitXmlWriter.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/JunitXmlWriter.java similarity index 95% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/JunitXmlWriter.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/JunitXmlWriter.java index ab1cc066f1b..4578d652b09 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/JunitXmlWriter.java +++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/JunitXmlWriter.java @@ -10,7 +10,9 @@ /** * This class allows to write test-results into XML like JUnit. - * https://stackoverflow.com/questions/4922867/what-is-the-junit-xml-format-specification-that-hudson-supports + * JUNIT + * Format * * @author Alexander Weigl * @version 1 (8/5/20) @@ -92,7 +94,7 @@ public void addTestcase( time)); } - enum TestCaseState { + public enum TestCaseState { FAILED, ERROR, SUCCESS, diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java similarity index 96% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java index ce99331dd7b..a1216597ec4 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java +++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java @@ -28,11 +28,10 @@ import org.key_project.logic.Name; import org.key_project.util.collection.Pair; +import org.junit.jupiter.api.Assertions; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import static org.junit.jupiter.api.Assertions.*; - /** * This class provides an API for running proves in JUnit test cases. @@ -48,7 +47,7 @@ * * @author Alexander Weigl * @version 1 (12.07.19) - * @see GenerateUnitTests + * @see GenerateUnitTestsUtil */ public class ProveTest { private static final Logger LOGGER = LoggerFactory.getLogger(ProveTest.class); @@ -97,7 +96,7 @@ private void runKey(String file, TestProperty testProperty) throws Exception { LOGGER.info("({}) Active Settings: {}", caseId, ProofSettings.DEFAULT_SETTINGS.settingsToString()); - assertTrue(Files.exists(keyFile), "File " + keyFile + " does not exists"); + Assertions.assertTrue(Files.exists(keyFile), "File " + keyFile + " does not exists"); // File that the created proof will be saved to. var proofFile = Paths.get(keyFile.toAbsolutePath() + ".proof"); @@ -125,11 +124,11 @@ private void runKey(String file, TestProperty testProperty) throws Exception { } if (testProperty == TestProperty.NOTLOADABLE) { - assertTrue(replayResult.hasErrors(), + Assertions.assertTrue(replayResult.hasErrors(), "Loading problem file succeeded but it shouldn't"); success = true; } else { - assertFalse(replayResult.hasErrors(), "Loading problem file failed"); + Assertions.assertFalse(replayResult.hasErrors(), "Loading problem file failed"); // For a reload test we are done at this point. Loading was successful. if (testProperty == TestProperty.LOADABLE) { @@ -167,7 +166,7 @@ private void runKey(String file, TestProperty testProperty) throws Exception { success ? " was successful " : " failed ", keyFile); if (!success) { - fail(message); + Assertions.fail(message); } } @@ -208,7 +207,7 @@ private void reload(Path proofFile, Proof loadedProof) throws Exception { ProofSaver.saveToFile(proofFile, loadedProof); boolean reloadedClosed = reloadProof(proofFile); - assertEquals(loadedProof.closed(), reloadedClosed, + Assertions.assertEquals(loadedProof.closed(), reloadedClosed, "Reloaded proof did not close: " + proofFile); debugOut("... success: reloaded."); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsDirectories.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsDirectories.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsDirectories.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsDirectories.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTest.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTest.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTest.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTest.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java similarity index 99% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java index 5f05662b563..4e3fd743fe2 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java +++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java @@ -5,6 +5,7 @@ import java.io.File; import java.io.IOException; +import java.io.Serial; import java.io.Serializable; import java.nio.file.Files; import java.nio.file.Path; @@ -23,8 +24,9 @@ * @author Kai Wallisch */ public final class RunAllProofsTestUnit implements Serializable { + @Serial private static final long serialVersionUID = -2406881153415390252L; - private static final Logger LOGGER = LoggerFactory.getLogger(StatisticsFile.class); + private static final Logger LOGGER = LoggerFactory.getLogger(RunAllProofsTestUnit.class); /** * The name of this test. diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/TestResult.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/TestResult.java similarity index 94% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/TestResult.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/TestResult.java index b5a846e5a9b..69ea36c2359 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/TestResult.java +++ b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/TestResult.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.runallproofs; +import java.io.Serial; import java.io.Serializable; /** @@ -10,6 +11,7 @@ * which specifies whether a test run was successful or not. */ public record TestResult(String message, boolean success) implements Serializable { + @Serial private static final long serialVersionUID = 7635762713077999920L; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingStrategy.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingStrategy.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingStrategy.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingStrategy.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTable.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTable.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTable.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTable.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/FunctionPerformanceData.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/FunctionPerformanceData.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/FunctionPerformanceData.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/FunctionPerformanceData.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/NodeData.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/NodeData.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/NodeData.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/NodeData.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/ProfilingDirectories.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/ProfilingDirectories.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/ProfilingDirectories.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/ProfilingDirectories.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleData.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleData.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleData.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleData.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleIndependentData.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleIndependentData.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleIndependentData.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleIndependentData.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkMode.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkMode.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkMode.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkMode.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkedTestFileRunner.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkedTestFileRunner.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkedTestFileRunner.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkedTestFileRunner.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/GroupedProofCollectionUnit.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/GroupedProofCollectionUnit.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/GroupedProofCollectionUnit.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/GroupedProofCollectionUnit.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionSettings.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionSettings.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionSettings.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionSettings.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionUnit.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionUnit.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionUnit.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollectionUnit.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/SingletonProofCollectionUnit.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/SingletonProofCollectionUnit.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/SingletonProofCollectionUnit.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/SingletonProofCollectionUnit.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/StatisticsFile.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/StatisticsFile.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/StatisticsFile.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/StatisticsFile.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestProperty.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestProperty.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestProperty.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestProperty.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/IOForwarder.java b/key.core/src/testFixtures/java/de/uka/ilkd/key/util/IOForwarder.java similarity index 100% rename from key.core/src/test/java/de/uka/ilkd/key/util/IOForwarder.java rename to key.core/src/testFixtures/java/de/uka/ilkd/key/util/IOForwarder.java diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/runallproofs/automaticJAVADL.properties b/key.core/src/testFixtures/resources/de/uka/ilkd/key/proof/runallproofs/automaticJAVADL.properties similarity index 100% rename from key.core/src/test/resources/de/uka/ilkd/key/proof/runallproofs/automaticJAVADL.properties rename to key.core/src/testFixtures/resources/de/uka/ilkd/key/proof/runallproofs/automaticJAVADL.properties diff --git a/key.ui/src/main/resources/logback.xml b/key.ui/src/main/resources/logback.xml deleted file mode 100644 index f22b587756a..00000000000 --- a/key.ui/src/main/resources/logback.xml +++ /dev/null @@ -1,56 +0,0 @@ - - - - - - - - ${user.home}/.key/logs/key_${timestamp}.log - false - - UTF-8 - - %date|%level|%thread|%logger|%file:%line|%replace(%msg){'[\n\r]','\\n'}|%replace(%ex){'[\n\r]','\\n'}%nopex|%n - true - - - - - - [%date{HH:mm:ss.SSS}] %highlight(%-5level) %cyan(%logger{0}) - %msg%ex%n - - - - INFO - - - - - - - - - - - - [%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n - - - TRACE - - - - - - - diff --git a/key.ui/src/test/resources/logback.xml b/key.ui/src/test/resources/logback.xml deleted file mode 100644 index eefd443474d..00000000000 --- a/key.ui/src/test/resources/logback.xml +++ /dev/null @@ -1,14 +0,0 @@ - - - - key.log - false - - %-10relative %-5level %-15thread %-25logger{5} %msg %ex%n - - - - - - - diff --git a/key.util/build.gradle b/key.util/build.gradle index cd0a45de4ae..63ea3fb5be5 100644 --- a/key.util/build.gradle +++ b/key.util/build.gradle @@ -1,7 +1,30 @@ +plugins { + id 'java-test-fixtures' +} + description = "Utility library of the key-project" dependencies { implementation("org.jspecify:jspecify:1.0.0") + + // we also export these dependency into src/test/java. + testFixturesApi(project(':key.util')) + + testFixturesApi(platform("org.junit:junit-bom:5.14.2")) + testFixturesApi("org.junit.jupiter:junit-jupiter-api") + testFixturesApi("org.junit.jupiter:junit-jupiter-params") + testFixturesApi("org.assertj:assertj-core:3.27.7") + testFixturesApi("ch.qos.logback:logback-classic:1.5.27") + testFixturesApi("org.jspecify:jspecify:1.0.0") + + testFixturesApi("ch.qos.logback:logback-classic:1.5.27") + + // test fixtures + testFixturesApi("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.0") + testFixturesApi("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.21.0") + + def eisop_version = "3.49.3-eisop1" + testFixturesCompileOnly( "io.github.eisop:checker-qual:$eisop_version") } checkerFramework { diff --git a/key.util/src/test/resources/logback.xml b/key.util/src/test/resources/logback.xml deleted file mode 100644 index 13617d11a78..00000000000 --- a/key.util/src/test/resources/logback.xml +++ /dev/null @@ -1,14 +0,0 @@ - - - - key.log - false - - %-10relative %-5level %-15thread %-25logger{5} %msg %ex{long}%n - - - - - - - \ No newline at end of file diff --git a/key.util/src/testFixtures/java/de/uka/ilkd/key/testfixtures/GithubTestPrinter.java b/key.util/src/testFixtures/java/de/uka/ilkd/key/testfixtures/GithubTestPrinter.java new file mode 100644 index 00000000000..58afda17f72 --- /dev/null +++ b/key.util/src/testFixtures/java/de/uka/ilkd/key/testfixtures/GithubTestPrinter.java @@ -0,0 +1,83 @@ +/* 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.testfixtures; + +import java.util.Optional; + +import org.junit.jupiter.api.extension.AfterAllCallback; +import org.junit.jupiter.api.extension.BeforeAllCallback; +import org.junit.jupiter.api.extension.ExtensionContext; +import org.junit.jupiter.api.extension.TestWatcher; + +/// A JUnit extension to print out workflow commands of Github actions to make logs more accessible. +/// +/// [See Github's +/// documentation.](https://docs.github.com/en/actions/reference/workflows-and-actions/workflow-commands#grouping-log-lines) +/// +/// @author Alexander Weigl +/// @version 1 (2026-02-23) +public class GithubTestPrinter implements TestWatcher, BeforeAllCallback, AfterAllCallback { + private static final boolean ENABLED = "true".equals(System.getenv("CI")); + + @Override + public void testAborted(ExtensionContext context, Throwable cause) { + if (ENABLED) { + return; + } + System.out.format("::error title=Test aborted %s::Test %s#%s aborted due to \"%s: %s\"%n", + context.getDisplayName(), + context.getRequiredTestClass().getName(), + context.getRequiredTestMethod().getName(), + cause.getClass().getName(), cause.getMessage()); + } + + @Override + public void testDisabled(ExtensionContext context, Optional reason) { + if (ENABLED) { + return; + } + System.out.format("::notice title=Disabled test %s::Test %s#%s disabled due to %s%n", + context.getDisplayName(), + context.getRequiredTestClass().getName(), + context.getRequiredTestMethod().getName(), + reason.orElse("no reason given")); + } + + @Override + public void testFailed(ExtensionContext context, Throwable cause) { + if (ENABLED) { + return; + } + System.out.format("::error title=Test failed %s::Test %s#%s aborted due to \"%s: %s\"%n", + context.getDisplayName(), + context.getRequiredTestClass().getName(), + context.getRequiredTestMethod().getName(), + cause.getClass().getName(), cause.getMessage()); + } + + @Override + public void testSuccessful(ExtensionContext context) { + if (ENABLED) { + return; + } + System.out.format("::debug::SUCCESS:%s%n", context.getDisplayName()); + } + + + @Override + public void beforeAll(ExtensionContext context) { + if (ENABLED) { + return; + } + System.out.format("::group::%s%n", context.getDisplayName()); + } + + @Override + public void afterAll(ExtensionContext context) { + if (ENABLED) { + return; + } + System.out.format("::endgroup::"); + } +} diff --git a/key.util/src/testFixtures/java/de/uka/ilkd/key/testfixtures/TestLogMgr.java b/key.util/src/testFixtures/java/de/uka/ilkd/key/testfixtures/TestLogMgr.java new file mode 100644 index 00000000000..fe0f06cae0c --- /dev/null +++ b/key.util/src/testFixtures/java/de/uka/ilkd/key/testfixtures/TestLogMgr.java @@ -0,0 +1,58 @@ +/* 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.testfixtures; + +import ch.qos.logback.classic.spi.ILoggingEvent; +import ch.qos.logback.core.ConsoleAppender; +import ch.qos.logback.core.encoder.LayoutWrappingEncoder; +import ch.qos.logback.core.testUtil.StringListAppender; +import org.junit.jupiter.api.extension.AfterTestExecutionCallback; +import org.junit.jupiter.api.extension.BeforeTestExecutionCallback; +import org.junit.jupiter.api.extension.ExtensionContext; +import org.slf4j.LoggerFactory; + +/** + * Extension of JUnit 5 that suppress logging of non-failing tests. + * + * @author Alexander Weigl + * @version 1 (2/17/26) + */ +public class TestLogMgr implements AfterTestExecutionCallback, BeforeTestExecutionCallback { + private static ch.qos.logback.classic.Logger root = + (ch.qos.logback.classic.Logger) LoggerFactory + .getLogger(org.slf4j.Logger.ROOT_LOGGER_NAME); + + private static final ConsoleAppender consoleAppender; + + private static final StringListAppender listAppender = + new StringListAppender<>(); + + static { + consoleAppender = (ConsoleAppender) root.getAppender("STDOUT"); + listAppender.setContext(consoleAppender.getContext()); + listAppender.setLayout( + ((LayoutWrappingEncoder) consoleAppender.getEncoder()).getLayout()); + listAppender.start(); + } + + @Override + public void afterTestExecution(ExtensionContext context) { + root.detachAppender(listAppender); + root.addAppender(consoleAppender); + if (context.getExecutionException().isPresent()) { + for (var s : listAppender.strList) { + System.out.print(s); + } + System.out.flush(); + } + listAppender.strList.clear(); + } + + @Override + public void beforeTestExecution(ExtensionContext context) { + System.out.flush(); + root.detachAppender(consoleAppender); + root.addAppender(listAppender); + } +} diff --git a/key.util/src/testFixtures/resources/META-INF/services/org.junit.jupiter.api.extension.Extension b/key.util/src/testFixtures/resources/META-INF/services/org.junit.jupiter.api.extension.Extension new file mode 100644 index 00000000000..cf9ce50c0f2 --- /dev/null +++ b/key.util/src/testFixtures/resources/META-INF/services/org.junit.jupiter.api.extension.Extension @@ -0,0 +1,2 @@ +de.uka.ilkd.key.testfixtures.TestLogMgr +de.uka.ilkd.key.testfixtures.GithubTestPrinter \ No newline at end of file diff --git a/key.util/src/testFixtures/resources/junit-platform.properties b/key.util/src/testFixtures/resources/junit-platform.properties new file mode 100644 index 00000000000..b059a65dc46 --- /dev/null +++ b/key.util/src/testFixtures/resources/junit-platform.properties @@ -0,0 +1 @@ +junit.jupiter.extensions.autodetection.enabled=true \ No newline at end of file diff --git a/key.core/src/test/resources/logback.xml b/key.util/src/testFixtures/resources/logback.xml similarity index 100% rename from key.core/src/test/resources/logback.xml rename to key.util/src/testFixtures/resources/logback.xml