Suppression of log for non-failing test classes

.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

.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:

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 {

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")))
 }
 
 

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}.
  * <p>
  * The considered proof collections files are configured statically in
- * {@link ProofCollections}.
+ * {@link InfFlowProofCollection}.
  *
  * @author Alexander Weigl
  * @version 1 (6/14/20)

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() {}
+}

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 {

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) {

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.
  * <p>
@@ -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);
     }
 }

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");

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() {}
+}

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)

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);
-    }
-
 }

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RunAllProofsTestWithComputeCostProfiling.java → key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestWithComputeCostProfiling.java

@@ -1,17 +1,15 @@
 /* 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;
 import java.util.Date;
 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;