Merge pull request #1474 from diffblue/jbmc

split up cbmc in cbmc and jbmc

Author: Daniel Kroening

regression/CMakeLists.txt

@@ -35,6 +35,7 @@ add_subdirectory(goto-diff)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(invariants)
+add_subdirectory(jbmc-strings)
 add_subdirectory(strings)
 add_subdirectory(strings-smoke-tests)
 add_subdirectory(test-script)

regression/Makefile

@@ -14,6 +14,7 @@ DIRS = ansi-c \
        goto-instrument-typedef \
        invariants \
        strings \
+       jbmc-strings \
        strings-smoke-tests \
        test-script \
        # Empty last line

regression/cbmc-java-inheritance/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:jbmc>"
 )

regression/cbmc-java-inheritance/Makefile

@@ -1,13 +1,13 @@
 default: tests.log
 
 test:
-	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi

regression/cbmc-java/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:jbmc>"
 )

regression/cbmc-java/Makefile

@@ -1,13 +1,13 @@
 default: tests.log
 
 test:
-	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi

regression/cbmc/trace_class_identifier/TestGenTest.class renamed to regression/cbmc-java/trace_class_identifier/TestGenTest.class

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

regression/cbmc/trace_class_identifier/TestGenTest.java renamed to regression/cbmc-java/trace_class_identifier/TestGenTest.java

@@ -0,0 +1,38 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+testfuture:
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc -CF ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+testall:
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc -CFTK ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+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
+