Skip to content

Commit db2f7b5

Browse files
peterschrammelpeterschrammel
committed
Use Maven to compile all regression test sources upfront (CMake)
This commit adds the CMake integration to call Maven to compile the test sources.
1 parent f9a7807 commit db2f7b5

File tree

4 files changed

+116
-6
lines changed

4 files changed

+116
-6
lines changed

‎jbmc/CMakeLists.txt

Lines changed: 24 additions & 4 deletions
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 clean package -T1C
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/pom.xml

Lines changed: 22 additions & 0 deletions
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

Lines changed: 68 additions & 0 deletions
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

Lines changed: 2 additions & 2 deletions
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)