Skip to content

Commit d2209c3

Browse files
peterschrammelpeterschrammel
committed
Use Maven to compile all regression test sources upfront
and give two examples of how this works: - jbmc/ArithmeticException1 (single source file) - jbmc/classpath-jar-load-whole-jar (jar)
1 parent 83f61a4 commit d2209c3

File tree

10 files changed

+154
-13
lines changed

10 files changed

+154
-13
lines changed

‎jbmc/CMakeLists.txt

+24-4
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,28 @@ add_custom_target(java-models-library ALL
3131
)
3232

3333
install(
34-
FILES
35-
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/core-models.jar"
36-
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/cprover-api.jar"
37-
DESTINATION ${CMAKE_INSTALL_LIBDIR}
34+
FILES
35+
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/core-models.jar"
36+
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/cprover-api.jar"
37+
DESTINATION ${CMAKE_INSTALL_LIBDIR}
38+
)
39+
40+
# java regression tests
41+
file(GLOB_RECURSE java_regression_sources "regression/**/*.java,regression/**/*.kt,regression/**/*.j,regression/**/pom.xml")
42+
file(GLOB java_regression_test_dirs LIST_DIRECTORIES true "regression/*/*")
43+
foreach(dir ${java_regression_test_dirs})
44+
# TODO: remove the last condition as soon as jbmc/deterministic_assignments_json has been converted
45+
IF(IS_DIRECTORY ${dir} AND EXISTS "${dir}/pom.xml" AND NOT EXISTS "${dir}/Foo.class")
46+
list(APPEND java_regression_compiled_sources "${dir}/target")
47+
ENDIF()
48+
endforeach()
49+
50+
add_custom_command(OUTPUT ${java_regression_compiled_sources}
51+
COMMAND ${MAVEN_PROGRAM} --quiet package
52+
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/regression
53+
DEPENDS ${java_regression_sources}
54+
)
55+
56+
add_custom_target(java-regression ALL
57+
DEPENDS ${java_regression_compiled_sources}
3858
)

‎jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class

-818 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException1/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException1</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException1/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

‎jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml

+7-6
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,15 @@
44
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
55
<modelVersion>4.0.0</modelVersion>
66
<groupId>org.cprover.regression</groupId>
7-
<artifactId>regression</artifactId>
7+
<artifactId>regression.jbmc.classpath-jar-load-whole-jar</artifactId>
88
<version>1.0-SNAPSHOT</version>
99

10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
1016
<build>
1117
<finalName>jar-file</finalName>
1218
<plugins>
@@ -24,9 +30,4 @@
2430
</plugins>
2531
</build>
2632

27-
<properties>
28-
<maven.compiler.source>1.8</maven.compiler.source>
29-
<maven.compiler.target>1.8</maven.compiler.target>
30-
</properties>
31-
3233
</project>

‎jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar

-4.35 KB
Binary file not shown.

‎jbmc/regression/jbmc/pom.xml

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
<packaging>pom</packaging>
10+
11+
<parent>
12+
<groupId>org.cprover.regression</groupId>
13+
<artifactId>regression</artifactId>
14+
<version>1.0-SNAPSHOT</version>
15+
</parent>
16+
17+
<modules>
18+
<module>ArithmeticException1</module>
19+
<module>classpath-jar-load-whole-jar</module>
20+
</modules>
21+
22+
</project>

‎jbmc/regression/pom.xml

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
<packaging>pom</packaging>
10+
11+
<properties>
12+
<maven.compiler.source>1.8</maven.compiler.source>
13+
<maven.compiler.target>1.8</maven.compiler.target>
14+
</properties>
15+
16+
<modules>
17+
<module>jbmc</module>
18+
</modules>
19+
20+
<build>
21+
<pluginManagement>
22+
<plugins>
23+
<plugin>
24+
<groupId>org.apache.maven.plugins</groupId>
25+
<artifactId>maven-jar-plugin</artifactId>
26+
<version>3.4.2</version>
27+
</plugin>
28+
<!-- turn off test running to save some time -->
29+
<plugin>
30+
<groupId>org.apache.maven.plugins</groupId>
31+
<artifactId>maven-surefire-plugin</artifactId>
32+
<version>3.5.2</version>
33+
<configuration>
34+
<skipTests>true</skipTests>
35+
</configuration>
36+
</plugin>
37+
<!-- turn off test compilation to save some time -->
38+
<plugin>
39+
<groupId>org.apache.maven.plugins</groupId>
40+
<artifactId>maven-compiler-plugin</artifactId>
41+
<version>3.13.0</version>
42+
<executions>
43+
<execution>
44+
<id>default-testCompile</id>
45+
<phase>test-compile</phase>
46+
<goals>
47+
<goal>testCompile</goal>
48+
</goals>
49+
<configuration>
50+
<skip>true</skip>
51+
</configuration>
52+
</execution>
53+
</executions>
54+
</plugin>
55+
<!-- turn off resources copying to save some time -->
56+
<plugin>
57+
<groupId>org.apache.maven.plugins</groupId>
58+
<artifactId>maven-resources-plugin</artifactId>
59+
<version>3.3.1</version>
60+
<configuration>
61+
<skip>true</skip>
62+
</configuration>
63+
</plugin>
64+
</plugins>
65+
</pluginManagement>
66+
</build>
67+
68+
</project>

‎jbmc/src/jbmc/CMakeLists.txt

+2-2
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,8 @@ add_executable(jbmc jbmc_main.cpp)
3232
target_link_libraries(jbmc jbmc-lib)
3333
install(TARGETS jbmc DESTINATION ${CMAKE_INSTALL_BINDIR})
3434

35-
# make sure java-models-library is built at least once
36-
add_dependencies(jbmc java-models-library)
35+
# make sure java-models-library and java-regression is built at least once
36+
add_dependencies(jbmc java-models-library java-regression)
3737

3838
# Man page
3939
if(NOT WIN32)

0 commit comments

Comments
 (0)