Move Java regression tests

Author: peterschrammel

jbmc/regression/CMakeLists.txt

@@ -0,0 +1,33 @@
+set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile};CBMC"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests cmdline)
+    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
+    message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
+endmacro(add_test_pl_tests)
+
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+add_subdirectory(jbmc)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(jbmc-strings)
+add_subdirectory(jdiff)
+add_subdirectory(janalyzer-taint)
+add_subdirectory(jbmc-concurrency)
+add_subdirectory(jbmc-inheritance)
+add_subdirectory(jbmc-cover)

jbmc/regression/Makefile

@@ -0,0 +1,53 @@
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+DIRS = janalzyer-taint \
+       jbmc \
+       jbmc-concurrency \
+       jbmc-cover \
+       jbmc-inheritance \
+       jbmc-strings \
+       jdiff \
+       string-smoke-tests \
+       # Empty last line
+
+# Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
+# the entire directory under Windows. This variable will contain the list
+# of directories that actually exist on the current platform.
+PLATFORM_DIRS = $(wildcard $(DIRS))
+
+# Run all test directories in sequence
+.PHONY: test
+test:
+	@for dir in $(PLATFORM_DIRS); do \
+		$(MAKE) "$$dir" || exit 1; \
+	done;
+
+# Pattern to execute a single test suite directory
+.PHONY: $(PLATFORM_DIRS)
+$(PLATFORM_DIRS):
+	@echo "Running $@..." ;
+	$(MAKE) -C "$@" test || exit 1;
+
+# Run all test directories using GNU Parallel
+.PHONY: test-parallel
+.NOTPARALLEL: test-parallel
+test-parallel:
+	@echo "Building with $(JOBS) jobs"
+	parallel \
+		--halt soon,fail=1 \
+		--tag \
+		--tagstring '{#}:' \
+		--linebuffer \
+		--jobs $(JOBS) \
+		$(MAKE) "{}" \
+		::: $(PLATFORM_DIRS)
+
+
+.PHONY: clean
+clean:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			$(MAKE) -C "$$dir" clean; \
+		fi; \
+	done;

jbmc/regression/janalyzer-taint/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:goto-analyzer>"
+)

jbmc/regression/janalyzer-taint/Makefile

@@ -0,0 +1,21 @@
+default: tests.log
+
+include ../../src/config.inc
+
+test:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-analyzer-taint/taint-aliasing1/aliasing1.class renamed to jbmc/regression/janalyzer-taint/taint-aliasing1/aliasing1.class

@@ -1,10 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/goto-analyzer-taint/taint-aliasing1/aliasing1.java renamed to jbmc/regression/janalyzer-taint/taint-aliasing1/aliasing1.java

@@ -1,10 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/goto-analyzer-taint/taint-aliasing1/taint.json renamed to jbmc/regression/janalyzer-taint/taint-aliasing1/taint.json

@@ -1,12 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/jbmc/jbmc
-	@../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/jbmc/jbmc
-	@../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/goto-analyzer-taint/taint-aliasing1/test.desc renamed to jbmc/regression/janalyzer-taint/taint-aliasing1/test.desc

@@ -0,0 +1,32 @@
+default: tests.log
+
+include ../../src/config.inc
+
+test:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+
+testfuture:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
+
+testall:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
+
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+