diff --git a/jbmc/CMakeLists.txt b/jbmc/CMakeLists.txt index 9b606f01185..561f89a5799 100644 --- a/jbmc/CMakeLists.txt +++ b/jbmc/CMakeLists.txt @@ -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 clean package -T1C + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/regression + DEPENDS ${java_regression_sources} +) + +add_custom_target(java-regression ALL + DEPENDS ${java_regression_compiled_sources} ) diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile index 4a052c618d7..c0f14f105c6 100644 --- a/jbmc/regression/Makefile +++ b/jbmc/regression/Makefile @@ -16,6 +16,7 @@ DIRS = janalyzer \ # Run all test directories in sequence .PHONY: test test: + mvn --quiet clean package -T1C @for dir in $(DIRS); do \ $(MAKE) "$$dir" || exit 1; \ done; @@ -30,6 +31,7 @@ $(DIRS): .PHONY: test-parallel .NOTPARALLEL: test-parallel test-parallel: + mvn --quiet clean package -T1C @echo "Building with $(JOBS) jobs" parallel \ --halt soon,fail=1 \ @@ -43,6 +45,7 @@ test-parallel: .PHONY: clean clean: + mvn --quiet clean -T1C @for dir in *; do \ if [ -d "$$dir" ]; then \ $(MAKE) -C "$$dir" clean; \ diff --git a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class deleted file mode 100644 index 3ad4e6ebe86..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException1/pom.xml b/jbmc/regression/jbmc/ArithmeticException1/pom.xml new file mode 100644 index 00000000000..898e619de4c --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException1/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException1/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException1/test.desc b/jbmc/regression/jbmc/ArithmeticException1/test.desc index 0577e08a51b..a07a8ddb801 100644 --- a/jbmc/regression/jbmc/ArithmeticException1/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException1/test.desc @@ -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$ diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml index ec40251b157..a87d85ac3bd 100644 --- a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml +++ b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml @@ -4,9 +4,15 @@ xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd"> 4.0.0 org.cprover.regression - regression + regression.jbmc.classpath-jar-load-whole-jar 1.0-SNAPSHOT + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + jar-file @@ -24,9 +30,4 @@ - - 1.8 - 1.8 - - diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar deleted file mode 100644 index d78794d6973..00000000000 Binary files a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar and /dev/null differ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml new file mode 100644 index 00000000000..9452e36ad45 --- /dev/null +++ b/jbmc/regression/jbmc/pom.xml @@ -0,0 +1,22 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + pom + + + org.cprover.regression + regression + 1.0-SNAPSHOT + + + + ArithmeticException1 + classpath-jar-load-whole-jar + + + diff --git a/jbmc/regression/pom.xml b/jbmc/regression/pom.xml new file mode 100644 index 00000000000..9cb0f685389 --- /dev/null +++ b/jbmc/regression/pom.xml @@ -0,0 +1,68 @@ + + + 4.0.0 + org.cprover.regression + regression + 1.0-SNAPSHOT + pom + + + 1.8 + 1.8 + + + + jbmc + + + + + + + org.apache.maven.plugins + maven-jar-plugin + 3.4.2 + + + + org.apache.maven.plugins + maven-surefire-plugin + 3.5.2 + + true + + + + + org.apache.maven.plugins + maven-compiler-plugin + 3.13.0 + + + default-testCompile + test-compile + + testCompile + + + true + + + + + + + org.apache.maven.plugins + maven-resources-plugin + 3.3.1 + + true + + + + + + + diff --git a/jbmc/src/jbmc/CMakeLists.txt b/jbmc/src/jbmc/CMakeLists.txt index 9010f0dd975..c1735e3ed94 100644 --- a/jbmc/src/jbmc/CMakeLists.txt +++ b/jbmc/src/jbmc/CMakeLists.txt @@ -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)