Seperate Java regression and unit tests from non-Java tests

This is a rather blunt change which could probably be done in a more
elegant way, but I'm trying to keep this patch as small as possible
with the view to later patches making bigger changes.

Author: chrisr-diffblue

CMakeLists.txt

@@ -77,6 +77,7 @@ set_target_properties(
     solvers
     test-bigint
     testing-utils
+    java-testing-utils
     unit
     util
     xml

regression/CMakeLists.txt

@@ -35,7 +35,7 @@ add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(strings)
 add_subdirectory(invariants)
-add_subdirectory(goto-diff)
+add_subdirectory(goto-diff-java)
 add_subdirectory(test-script)
 add_subdirectory(goto-analyzer-taint)
 add_subdirectory(cbmc-java-inheritance)
@@ -45,4 +45,5 @@ endif()
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
+add_subdirectory(goto-diff)
 

regression/Makefile

@@ -14,14 +14,15 @@ DIRS = cbmc \
        smt2_solver \
        strings \
        invariants \
-       goto-diff \
+       goto-diff-java \
        test-script \
        goto-analyzer-taint \
        cbmc-java-inheritance \
        goto-gcc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
+       goto-diff \
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks

regression/goto-diff-java/CMakeLists.txt

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

regression/goto-diff-java/Makefile

@@ -0,0 +1,18 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/goto-diff/goto-diff
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/goto-diff/goto-diff
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-diff/java-add-package/new.jar renamed to regression/goto-diff-java/java-add-package/new.jar

@@ -2,6 +2,10 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 
 file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
 
+file(GLOB_RECURSE java_testing_utils
+    "java_bytecode/testing-utils/*.cpp"
+    "java_bytecode/testing-utils/*.h")
+
 list(REMOVE_ITEM sources
     # Used in executables
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
@@ -21,12 +25,14 @@ list(REMOVE_ITEM sources
 
     # Will be built into a separate library and linked
     ${testing_utils}
+    ${java_testing_utils}
 
     # Intended to fail to compile
     ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
 )
 
 add_subdirectory(testing-utils)
+add_subdirectory(java_bytecode/testing-utils)
 
 add_executable(unit ${sources})
 target_include_directories(unit
@@ -38,6 +44,7 @@ target_include_directories(unit
 target_link_libraries(
         unit
         testing-utils
+        java-testing-utils
         ansi-c
         solvers
         java_bytecode

regression/goto-diff/java-add-package/new/Test.java renamed to regression/goto-diff-java/java-add-package/new/Test.java

@@ -13,9 +13,9 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
-       goto-programs/class_hierarchy_output.cpp \
-       goto-programs/class_hierarchy_graph.cpp \
-       goto-programs/remove_virtual_functions_without_fallback.cpp \
+       java_bytecode/goto-programs/class_hierarchy_output.cpp \
+       java_bytecode/goto-programs/class_hierarchy_graph.cpp \
+       java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \
        java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
@@ -31,26 +31,28 @@ SRC += unit_tests.cpp \
        java_bytecode/java_utils_test.cpp \
        java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
        path_strategies.cpp \
-       pointer-analysis/custom_value_set_analysis.cpp \
+       java_bytecode/pointer-analysis/custom_value_set_analysis.cpp \
        sharing_node.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
-       solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
+       java_bytecode/solvers_instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
-       solvers/refinement/string_refinement/dependency_graph.cpp \
+       java_bytecode/solvers_dependency_graph.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
-       solvers/refinement/string_refinement/string_symbol_resolution.cpp \
+       java_bytecode/solvers_string_symbol_resolution.cpp \
        solvers/refinement/string_refinement/sparse_array.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
        util/has_subtype.cpp \
+       java_bytecode/util/has_subtype.cpp \
        util/irep.cpp \
        util/irep_sharing.cpp \
        util/message.cpp \
        util/optional.cpp \
-       util/parameter_indices.cpp \
+       java_bytecode/util/parameter_indices.cpp \
+       java_bytecode/util/simplify_expr.cpp \
        util/simplify_expr.cpp \
        util/small_shared_two_way_ptr.cpp \
        util/string_utils/split_string.cpp \
@@ -62,6 +64,7 @@ SRC += unit_tests.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.
+INCLUDES+= -I ./java_bytecode
 
 include ../src/config.inc
 include ../src/common
@@ -72,6 +75,9 @@ cprover.dir:
 testing-utils.dir:
 	$(MAKE) $(MAKEARGS) -C testing-utils
 
+java-testing-utils.dir:
+	$(MAKE) $(MAKEARGS) -C java_bytecode/testing-utils
+
 # We need to link bmc.o to the unit test, so here's everything it depends on...
 BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/bmc$(OBJEXT) \
@@ -118,15 +124,17 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(BMC_DEPS)
               # Empty last line
 
-OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT)
+OBJ +=  $(CPROVER_LIBS) \
+        testing-utils/testing-utils$(LIBEXT) \
+        java_bytecode/testing-utils/java-testing-utils$(LIBEXT) 
 
 TESTS = unit_tests$(EXEEXT) \
         miniBDD$(EXEEXT) \
         # Empty last line
 
 CLEANFILES = $(TESTS)
 
-all: cprover.dir testing-utils.dir
+all: cprover.dir testing-utils.dir java-testing-utils.dir
 	$(MAKE) $(MAKEARGS) $(TESTS)
 
 test: all

regression/goto-diff/java-add-package/old.jar renamed to regression/goto-diff-java/java-add-package/old.jar

@@ -28,10 +28,10 @@ void require_parent_child_relationship(
 
 SCENARIO(
   "Output a simple class hierarchy"
-  "[core][goto-programs][class_hierarchy_graph]")
+  "[core][java_bytecode][goto-programs][class_hierarchy_graph]")
 {
   symbol_tablet symbol_table =
-    load_java_class("HierarchyTest", "goto-programs/");
+    load_java_class("HierarchyTest", "java_bytecode/goto-programs/");
   class_hierarchy_grapht hierarchy;
   hierarchy.populate(symbol_table);
 

regression/goto-diff/java-add-package/old/Test.java renamed to regression/goto-diff-java/java-add-package/old/Test.java

@@ -37,10 +37,10 @@ void require_parent_child_relationship(
 
 SCENARIO(
   "Output a simple class hierarchy"
-  "[core][goto-programs][class_hierarchy]")
+  "[core][java_bytecode][goto-programs][class_hierarchy]")
 {
   symbol_tablet symbol_table =
-    load_java_class("HierarchyTest", "goto-programs/");
+    load_java_class("HierarchyTest", "java_bytecode/goto-programs/");
   class_hierarchyt hierarchy;
 
   std::stringstream output_stream;

regression/goto-diff/java-add-package/test.desc renamed to regression/goto-diff-java/java-add-package/test.desc

@@ -19,15 +19,15 @@
 
 SCENARIO(
   "Instantiate generic parameters of superclasses",
-  "[core][goto_program_generics][generic_bases_test]")
+  "[core][java_bytecode][goto_program_generics][generic_bases_test]")
 {
   GIVEN(
     "A class extending a generic class instantiated with a standard library "
     "class")
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInst",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassInst.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -68,7 +68,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInst2",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassInst2.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -99,7 +99,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInst3",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassInst3.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -142,7 +142,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassUninstTest",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassUninstTest.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -187,7 +187,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassMixedTest",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassMixedTest.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -240,7 +240,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInnerInst",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassInnerInst.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -309,7 +309,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassInnerUninstTest",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassInnerUninstTest.foo");
 
     WHEN("The method input argument is created in the entry point function")
@@ -417,15 +417,15 @@ SCENARIO(
 
 SCENARIO(
   "Ignore generics for incomplete and non-generic bases",
-  "[core][goto_program_generics][generic_bases_test]")
+  "[core][java_bytecode][goto_program_generics][generic_bases_test]")
 {
   GIVEN(
     "A class extending a generic class with unsupported class signature (thus"
     " not marked as generic)")
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassUnsupported",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassUnsupported.foo");
 
     THEN("The struct for UnsupportedWrapper1 is complete and non-generic")
@@ -474,7 +474,7 @@ SCENARIO(
   {
     const symbol_tablet &symbol_table = load_java_class(
       "SuperclassOpaque",
-      "./goto-programs/goto_program_generics",
+      "./java_bytecode/goto-programs/goto_program_generics",
       "SuperclassOpaque.foo");
 
     THEN("The struct for OpaqueWrapper is incomplete and not-generic")