Skip to content
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

Jump to bottom

Compile Java regression test sources (1/n) #8487

Draft
wants to merge 4 commits into
base: develop
Choose a base branch
from
Draft

Compile Java regression test sources (1/n) #8487

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1770482
Use Maven to compile all regression test sources upfront
peterschrammel Nov 10, 2024
26a496e
Compile jbmc/ArithmeticException1 test sources
peterschrammel Nov 10, 2024
a1ff4b7
Compile jbmc/classpath-jar-load-whole-jar test sources
peterschrammel Nov 10, 2024
9e595aa
Use cmake for cleaning in cmake job
peterschrammel Nov 12, 2024
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
4 changes: 1 addition & 3 deletions .github/workflows/pull-request-checks.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,11 +263,9 @@ jobs:
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
- name: Check cleanup
run: |
cmake --build build --target clean
rm -r build
rm scripts/bash-autocomplete/cbmc.sh
make -C unit clean
make -C regression clean
make -C jbmc/regression clean
if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
git status --ignored
exit 1
Expand Down
28 changes: 24 additions & 4 deletions jbmc/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,28 @@ add_custom_target(java-models-library ALL
)

install(
FILES
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/core-models.jar"
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/cprover-api.jar"
DESTINATION ${CMAKE_INSTALL_LIBDIR}
FILES
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/core-models.jar"
"${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/cprover-api.jar"
DESTINATION ${CMAKE_INSTALL_LIBDIR}
)

# java regression tests
file(GLOB_RECURSE java_regression_sources "regression/**/*.java,regression/**/*.kt,regression/**/*.j,regression/**/pom.xml")
file(GLOB java_regression_test_dirs LIST_DIRECTORIES true "regression/*/*")
foreach(dir ${java_regression_test_dirs})
# TODO: remove the last condition as soon as jbmc/deterministic_assignments_json has been converted
IF(IS_DIRECTORY ${dir} AND EXISTS "${dir}/pom.xml" AND NOT EXISTS "${dir}/Foo.class")
list(APPEND java_regression_compiled_sources "${dir}/target")
ENDIF()
endforeach()

add_custom_command(OUTPUT ${java_regression_compiled_sources}
COMMAND ${MAVEN_PROGRAM} --quiet package
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/regression
DEPENDS ${java_regression_sources}
)

add_custom_target(java-regression ALL
DEPENDS ${java_regression_compiled_sources}
)
Binary file removed jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException1/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.jbmc.ArithmeticException1</artifactId>
<version>1.0-SNAPSHOT</version>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.jbmc</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<build>
<plugins>
<plugin>
<artifactId>maven-jar-plugin</artifactId>
<executions>
<execution>
<id>default-jar</id>
<phase>none</phase>
</execution>
</executions>
</plugin>
</plugins>
</build>

</project>
0 ...icException1/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
ArithmeticExceptionTest
--throw-runtime-exceptions
--throw-runtime-exceptions -cp target/classes
^EXIT=10$
^SIGNAL=0$
^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
Expand Down
13 changes: 7 additions & 6 deletions jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,15 @@
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>org.cprover.regression</groupId>
<artifactId>regression</artifactId>
<artifactId>regression.jbmc.classpath-jar-load-whole-jar</artifactId>
<version>1.0-SNAPSHOT</version>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.jbmc</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<build>
<finalName>jar-file</finalName>
<plugins>
Expand All @@ -24,9 +30,4 @@
</plugins>
</build>

<properties>
<maven.compiler.source>1.8</maven.compiler.source>
<maven.compiler.target>1.8</maven.compiler.target>
</properties>

</project>
Binary file removed jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar
View file
Open in desktop
Binary file not shown.
22 changes: 22 additions & 0 deletions jbmc/regression/jbmc/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.jbmc</artifactId>
<version>1.0-SNAPSHOT</version>
<packaging>pom</packaging>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<modules>
<module>ArithmeticException1</module>
<module>classpath-jar-load-whole-jar</module>
</modules>

</project>
68 changes: 68 additions & 0 deletions jbmc/regression/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>org.cprover.regression</groupId>
<artifactId>regression</artifactId>
<version>1.0-SNAPSHOT</version>
<packaging>pom</packaging>

<properties>
<maven.compiler.source>1.8</maven.compiler.source>
<maven.compiler.target>1.8</maven.compiler.target>
</properties>

<modules>
<module>jbmc</module>
</modules>

<build>
<pluginManagement>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-jar-plugin</artifactId>
<version>3.4.2</version>
</plugin>
<!-- turn off test running to save some time -->
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-surefire-plugin</artifactId>
<version>3.5.2</version>
<configuration>
<skipTests>true</skipTests>
</configuration>
</plugin>
<!-- turn off test compilation to save some time -->
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.13.0</version>
<executions>
<execution>
<id>default-testCompile</id>
<phase>test-compile</phase>
<goals>
<goal>testCompile</goal>
</goals>
<configuration>
<skip>true</skip>
</configuration>
</execution>
</executions>
</plugin>
<!-- turn off resources copying to save some time -->
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-resources-plugin</artifactId>
<version>3.3.1</version>
<configuration>
<skip>true</skip>
</configuration>
</plugin>
</plugins>
</pluginManagement>
</build>

</project>
4 changes: 2 additions & 2 deletions jbmc/src/jbmc/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ add_executable(jbmc jbmc_main.cpp)
target_link_libraries(jbmc jbmc-lib)
install(TARGETS jbmc DESTINATION ${CMAKE_INSTALL_BINDIR})

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

# Man page
if(NOT WIN32)
Expand Down
Loading