Skip to content

Migrate to JUnit6 #681

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
daniel-raffler wants to merge 20 commits into
base: master
Choose a base branch
from
Draft

Migrate to JUnit6 #681

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
8ba8266
Change dependencies to JUnit6 and update classpath
daniel-raffler May 31, 2026
dcab8ab
Update test classes
daniel-raffler May 31, 2026
0910719
Update ant build
daniel-raffler May 31, 2026
c3e5c5b
Restore SolverBasedTest0 to JUnit4 so as not to break the API
daniel-raffler May 31, 2026
19e2413
Remove unused throw annotation
daniel-raffler May 31, 2026
b8e33db
Get `junitlauncher` task from Maven if it's not included in the ant d…
daniel-raffler May 31, 2026
2a3831f
Suppress spotbug warnings about unread fields in SolverBasedTest0
daniel-raffler May 31, 2026
2d53a07
Fix loading of junitlauncher
daniel-raffler May 31, 2026
41f7951
Use @EnumSource for solver based tests
daniel-raffler Jun 5, 2026
a0a9bc7
Fix copyright data in new class
daniel-raffler Jun 5, 2026
26a96cb
Make SolverBasedTest non-abstract
daniel-raffler Jun 12, 2026
517fcad
Update JavaDocs
daniel-raffler Jun 12, 2026
f01f35b
Merge branch 'master' into junit6-noNested
daniel-raffler Jun 12, 2026
360ee6f
Format
daniel-raffler Jun 12, 2026
7686a4f
Suppress native access warnings while running the tests
daniel-raffler Jun 22, 2026
249f2dc
Add dependency on junit4 vintage runner to enable PackageSanityTests
daniel-raffler Jun 22, 2026
94746ef
Use ParameterizedSolverBasedTest.getAllSolvers() in TranslateFormulaT…
daniel-raffler Jun 22, 2026
c348db6
Exclude abstract base classes from tests
daniel-raffler Jun 22, 2026
8122cff
Remove unused import
daniel-raffler Jun 22, 2026
2f3c59c
Use opentest format for generating the test report
daniel-raffler Jun 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion .classpath
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,14 @@ SPDX-License-Identifier: Apache-2.0
<classpathentry kind="lib" path="lib/java/core/guava.jar" sourcepath="lib/java-contrib/guava-sources.jar"/>
<classpathentry kind="lib" path="lib/java/test/guava-testlib.jar" sourcepath="lib/java-contrib/guava-testlib-sources.jar"/>
<classpathentry kind="lib" path="lib/java/test/truth.jar" sourcepath="lib/java-contrib/truth-sources.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-jupiter-api.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-jupiter-engine.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-jupiter-params.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-platform-commons.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-platform-console.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-platform-engine.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-platform-launching.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit-platform-reporting.jar"/>
<classpathentry kind="lib" path="lib/java/test/hamcrest-core.jar"/>
<classpathentry kind="lib" path="lib/java/core/spotbugs-annotations.jar" sourcepath="lib/java-contrib/spotbugs-annotations-sources.jar"/>
<classpathentry kind="lib" path="lib/java/core/jsr305.jar" sourcepath="lib/java-contrib/jsr305-sources.jar"/>
Expand Down
93 changes: 55 additions & 38 deletions build/build-junit.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,15 +29,15 @@ SPDX-License-Identifier: Apache-2.0

<!-- Load the JUnit plugin for Ant if it's not installed. -->
<condition property="ant.junit.available">
<typefound name="junit"/>
<typefound name="junitlauncher"/>
</condition>
<target name="load-junit" depends="resolve-dependencies" unless="ant.junit.available">
<taskdef name="junit"
classname="org.apache.tools.ant.taskdefs.optional.junit.JUnitTask"
classpath="${ivy.jar.dir}/ant-junit.jar:${ivy.jar.dir}/ant-junit4.jar"/>
<taskdef name="junitlauncher"
classname="org.apache.tools.ant.taskdefs.optional.junitlauncher.confined.JUnitLauncherTask"
classpath="${ivy.jar.dir}/ant-junitlauncher.jar:${ivy.jar.dir}/ant-junit.jar"/>
<taskdef name="junitreport"
classname="org.apache.tools.ant.taskdefs.optional.junit.XMLResultAggregator"
classpath="${ivy.jar.dir}/ant-junit.jar:${ivy.jar.dir}/ant-junit4.jar"/>
classpath="${ivy.jar.dir}/ant-junit.jar"/>
</target>

<target name="init-unit-tests">
Expand All @@ -51,25 +51,34 @@ SPDX-License-Identifier: Apache-2.0
</target>

<macrodef name="run-junit-tests">
<sequential>
<junit fork="true" printSummary="true" showOutput="false" failureproperty="junit.failed" timeout="600000">
<assertions><enable/></assertions>
<formatter type="xml"/>
<classpath refid="classpath.junit"/>
<sysproperty key="java.awt.headless" value="true" />
<batchtest fork="true" todir="${junit.dir}">
<fileset dir="${class.dir}">
<patternset refid="test.sources"/>
</fileset>
</batchtest>
</junit>
<junitreport todir="${junit.dir}">
<fileset dir="${junit.dir}" includes="TEST-*.xml"/>
<report format="noframes"/>
</junitreport>
<move file="junit-noframes.html" tofile="JUnit.html"/>
<fail if="junit.failed" message="JUnit tests failed, look at JUnit.html"/>
</sequential>
<sequential>
<junitlauncher printsummary="true" failureproperty="junit.failed">
<classpath refid="classpath.junit"/>
<testclasses>
<fork forkmode="perTestClass">
<sysproperty key="junit.platform.reporting.open.xml.enabled" value="true"/>
<sysproperty key="junit.platform.reporting.output.dir" value="${junit.dir}/{uniqueNumber}"/>
<sysproperty key="java.awt.headless" value="true"/>
<jvmarg value="-ea"/>
<jvmarg value="--enable-native-access=ALL-UNNAMED"/>
</fork>
<fileset dir="${class.dir}">
<patternset refid="test.sources"/>
</fileset>
</testclasses>
</junitlauncher>
<fileset id="opentest.reports" dir="${junit.dir}" includes="**/*.xml"/>
<pathconvert refid="opentest.reports" property="reports" pathsep=" "/>
<!-- Generate the html report -->
<java classname="org.opentest4j.reporting.cli.ReportingCli">
<classpath refid="classpath.junit"/>
<arg value="html-report"/>
<arg value="--output"/>
<arg value="JUnit.html"/>
<arg line="${reports}"/>
</java>
<fail if="junit.failed" message="JUnit tests failed, look at JUnit.html"/>
</sequential>
</macrodef>

<target name="unit-tests-quick" depends="build, load-junit, init-unit-tests"
Expand Down Expand Up @@ -103,6 +112,8 @@ SPDX-License-Identifier: Apache-2.0
<patternset id="test.sources">
<include name="**/*Test.*"/>
<exclude name="**/*$*Test.*"/>
<exclude name="**/SolverBasedTest.*"/>
<exclude name="**/Mathsat5AbstractNativeApiTest.*"/>
</patternset>
<run-junit-tests/>
</target>
Expand All @@ -114,20 +125,26 @@ SPDX-License-Identifier: Apache-2.0
</target>

<target name="unit-tests-coverage" depends="build, load-junit, load-jacoco, init-unit-tests" description="Run all JUnit tests with coverage report">
<jacoco:coverage destfile="${junit.dir}/jacoco.exec" excludes="**/*Test*:**/Dummy*">
<junit fork="true" printSummary="true" showOutput="false" failureproperty="junit.failed" timeout="600000">
<assertions><enable/></assertions>
<formatter type="xml"/>
<classpath refid="classpath.junit"/>
<sysproperty key="java.awt.headless" value="true" />
<batchtest fork="true" todir="${junit.dir}">
<fileset dir="${class.dir}">
<include name="**/*Test.*"/>
<exclude name="**/*$*Test.*"/>
</fileset>
</batchtest>
</junit>
</jacoco:coverage>
<jacoco:agent property="jacocoagent" destfile="${junit.dir}/jacoco.exec"/>
<junitlauncher printsummary="true" failureproperty="junit.failed">
<classpath refid="classpath.junit"/>
<testclasses outputdir="${junit.dir}">
<fork forkmode="perTestClass">
<sysproperty key="java.awt.headless" value="true"/>
<jvmarg value="${jacocoagent}"/>
<jvmarg value="-ea"/>
<jvmarg value="--enable-native-access=ALL-UNNAMED"/>
</fork>
<fileset dir="${class.dir}">
<include name="**/*Test.*"/>
<exclude name="**/*$*Test.*"/>
<exclude name="**/SolverBasedTest.*"/>
<exclude name="**/Mathsat5AbstractNativeApiTest.*"/>
</fileset>
<listener type="legacy-brief" sendSysOut="true"/>
<listener type="legacy-xml" sendSysErr="true" sendSysOut="true"/>
</testclasses>
</junitlauncher>
<jacoco:report>
<executiondata><file file="${junit.dir}/jacoco.exec"/></executiondata>
<structure name="${ant.project.name}">
Expand Down
15 changes: 10 additions & 5 deletions build/ivysettings.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,19 @@ SPDX-License-Identifier: Apache-2.0
Keep this file synchronized with
https://gitlab.com/sosy-lab/software/java-project-template
-->
<settings defaultResolver="Sosy-Lab"/>
<settings defaultResolver="default"/>
<property name="repo.dir" value="${basedir}/repository"/>
<resolvers>
<!-- Resolver for downloading dependencies -->
<url name="Sosy-Lab" descriptor="required">
<ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml" />
<artifact pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]" />
</url>
<chain name="default">
<!-- Download packages from Sosy-Labs -->
<url name="Sosy-Lab" descriptor="required">
<ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml"/>
<artifact pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/>
</url>
<!-- Use Maven central as a fallback -->
<ibiblio name="central" m2compatible="true"/>
</chain>

<!-- Resolver for publishing this project -->
<filesystem name="Sosy-Lab-Publish">
Comment on lines 15 to 33

@daniel-raffler daniel-raffler Jun 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can be reverted once we have ant-junitlauncher from org.apache.ant in Ivy

Expand Down
14 changes: 12 additions & 2 deletions lib/ivy.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,17 @@ SPDX-License-Identifier: Apache-2.0

<!-- JUnit
Testing framework. -->
<dependency org="junit" name="junit" rev="4.13.2" conf="test->default; contrib->sources"/>
<dependency org="org.junit.jupiter" name="junit-jupiter-api" rev="6.1.0" conf="test->default"/>
<dependency org="org.junit.jupiter" name="junit-jupiter-params" rev="6.1.0" conf="test->default"/>
<dependency org="org.junit.jupiter" name="junit-jupiter-engine" rev="6.1.0" conf="test->default"/>
<dependency org="org.junit.vintage" name="junit-vintage-engine" rev="6.1.0" conf="test->default"/>

<dependency org="org.junit.platform" name="junit-platform-launcher" rev="6.1.0" conf="test->default"/>
<dependency org="org.junit.platform" name="junit-platform-reporting" rev="6.1.0" conf="test->default"/>

<!-- Open Test Reporting
CLI tool for generate test reports -->
<dependency org="org.opentest4j.reporting" name="open-test-reporting-cli" rev="0.2.5" conf="test->default"/>

<!-- JaCoCo
Library for code coverage -->
Expand All @@ -138,7 +148,7 @@ SPDX-License-Identifier: Apache-2.0
<!-- The JUnit task for Ant so that we can run the tests.
The property used here is defined in build.xml according to the current Ant version. -->
<dependency org="org.apache.ant" name="ant-junit" rev="${ant.version.exact}" transitive="false" conf="build->default"/>
<dependency org="org.apache.ant" name="ant-junit4" rev="${ant.version.exact}" transitive="false" conf="build->default"/>
<dependency org="org.apache.ant" name="ant-junitlauncher" rev="${ant.version.exact}" transitive="false" conf="build->default"/>

<!-- Truth
Library for writing literal assertions. -->
Expand Down
24 changes: 12 additions & 12 deletions src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaNativeApiTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,16 +9,16 @@
package org.sosy_lab.java_smt.solvers.bitwuzla;

import static com.google.common.truth.Truth.assertThat;
import static org.junit.Assert.assertThrows;
import static org.junit.jupiter.api.Assertions.assertThrows;
import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext.loadLibrary;

import com.google.common.truth.Truth;
import org.junit.After;
import org.junit.AssumptionViolatedException;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Ignore;
import org.junit.Test;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Disabled;
import org.junit.jupiter.api.Test;
import org.opentest4j.TestAbortedException;
import org.sosy_lab.common.NativeLibraries;
import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla;
import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind;
Expand All @@ -39,16 +39,16 @@ public class BitwuzlaNativeApiTest {
private TermManager termManager;
private Bitwuzla bitwuzla;

@BeforeClass
@BeforeAll
public static void load() {
try {
loadLibrary(NativeLibraries::loadLibrary);
} catch (UnsatisfiedLinkError e) {
throw new AssumptionViolatedException("Bitwuzla is not available", e);
throw new TestAbortedException("Bitwuzla is not available", e);
}
}

@Before
@BeforeEach
public void createEnvironment() {
termManager = new TermManager();
bitwuzla = new Bitwuzla(termManager, createOptions());
Expand All @@ -60,7 +60,7 @@ private Options createOptions() {
return options;
}

@After
@AfterEach
public void freeEnvironment() {
TermManager.deleteReferences();
}
Expand Down Expand Up @@ -772,7 +772,7 @@ private Vector_Term parse(String smt2dump) {
}

// Bitwuzla currently REWRITES terms when parsing
@Ignore
@Disabled
@Test
public void parserTest2() {
Vector_Term assertions = parse(SMT2DUMP);
Expand Down
18 changes: 9 additions & 9 deletions src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,11 @@
import com.google.common.collect.ImmutableMap;
import java.util.Arrays;
import java.util.Locale;
import org.junit.After;
import org.junit.AssumptionViolatedException;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;
import org.opentest4j.TestAbortedException;
import org.sosy_lab.common.NativeLibraries;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.common.configuration.Configuration;
Expand All @@ -35,21 +35,21 @@ public class BoolectorNativeApiTest {

private long btor;

@BeforeClass
@BeforeAll
public static void load() {
try {
NativeLibraries.loadLibrary("boolector");
} catch (UnsatisfiedLinkError e) {
throw new AssumptionViolatedException("Boolector is not available", e);
throw new TestAbortedException("Boolector is not available", e);
}
}

@Before
@BeforeEach
public void createEnvironment() {
btor = BtorJNI.boolector_new();
}

@After
@AfterEach
public void freeEnvironment() {
BtorJNI.boolector_delete(btor);
}
Expand Down
20 changes: 10 additions & 10 deletions src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
package org.sosy_lab.java_smt.solvers.cvc4;

import static com.google.common.truth.Truth.assertThat;
import static org.junit.Assert.assertThrows;
import static org.junit.jupiter.api.Assertions.assertThrows;

import edu.stanford.CVC4.ArrayType;
import edu.stanford.CVC4.BitVector;
Expand All @@ -29,11 +29,11 @@
import edu.stanford.CVC4.Type;
import edu.stanford.CVC4.UnsatCore;
import edu.stanford.CVC4.vectorExpr;
import org.junit.After;
import org.junit.AssumptionViolatedException;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeAll;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;
import org.opentest4j.TestAbortedException;
import org.sosy_lab.common.NativeLibraries;

/*
Expand All @@ -58,19 +58,19 @@ public class CVC4NativeAPITest {
private Expr aAtxEq0;
private Expr aAtxEq1;

@BeforeClass
@BeforeAll
public static void loadCVC4() {
try {
NativeLibraries.loadLibrary("cvc4jni");
} catch (UnsatisfiedLinkError e) {
throw new AssumptionViolatedException("CVC4 is not available", e);
throw new TestAbortedException("CVC4 is not available", e);
}
}

private ExprManager exprMgr;
private SmtEngine smtEngine;

@Before
@BeforeEach
public void createEnvironment() {
exprMgr = new ExprManager();
smtEngine = new SmtEngine(exprMgr);
Expand All @@ -84,7 +84,7 @@ public void createEnvironment() {
smtEngine.setOption("output-language", new SExpr("smt2"));
}

@After
@AfterEach
public void freeEnvironment() {
smtEngine.delete();
exprMgr.delete();
Expand Down
Loading
Loading