unit test Makefiles: add missing source files

CMakeLists.txt

@@ -68,7 +68,6 @@ set_target_properties(
     json
     langapi
     linking
-    miniBDD
     pointer-analysis
     solvers
     test-bigint

jbmc/regression/jbmc-generics/Makefile

@@ -20,7 +20,7 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log tests-symex-driven-loading.log
 
 %.class: %.java ../../src/org.cprover.jar
 	javac -g -cp ../../src/org.cprover.jar:. $<

jbmc/regression/strings-smoke-tests/Makefile

@@ -28,4 +28,4 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log tests-symex-driven-loading.log

jbmc/unit/Makefile

@@ -1,30 +1,53 @@
-.PHONY: all cprover.dir jprover.dir testing-utils.dir java-testing-utils.dir test
+.PHONY: all jprover.dir test java-testing-utils-clean
 
 # Source files for test utilities
 SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \
       # Empty last line
 
 # Test source files
-SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
+SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
+       java_bytecode/expr2java.cpp \
+       java_bytecode/goto_program_generics/generic_bases_test.cpp \
+       java_bytecode/goto_program_generics/generic_parameters_test.cpp \
+       java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \
        java_bytecode/goto-programs/class_hierarchy_graph.cpp \
+       java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \
+       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
        java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
        java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
+       java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
+       java_bytecode/java_bytecode_convert_method/convert_method.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
-       java_bytecode/java_bytecode_parser/parse_java_class.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \
+       java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \
+       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
+       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
+       java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \
        java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
+       java_bytecode/java_bytecode_parser/parse_java_class.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
-       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
-       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
+       java_bytecode/java_replace_nondet/replace_nondet.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        java_bytecode/java_types/erase_type_arguments.cpp \
        java_bytecode/java_types/generic_type_index.cpp \
        java_bytecode/java_types/java_generic_symbol_type.cpp \
        java_bytecode/java_types/java_type_from_string.cpp \
        java_bytecode/java_utils_test.cpp \
+       java_bytecode/java_virtual_functions/virtual_functions.cpp \
        java_bytecode/load_method_by_regex.cpp \
-       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
        pointer-analysis/custom_value_set_analysis.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/dependency_graph.cpp \
@@ -33,9 +56,6 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        util/has_subtype.cpp \
        util/parameter_indices.cpp \
        util/simplify_expr.cpp \
-       java_bytecode/java_virtual_functions/virtual_functions.cpp \
-       java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
-       java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit
@@ -44,18 +64,18 @@ include ../src/config.inc
 include $(CPROVER_DIR)/src/config.inc
 include $(CPROVER_DIR)/src/common
 
-cprover.dir:
-	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src
-
 jprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src
 
-cprover-testing-utils.dir:
+$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT): jprover.dir
 	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils
 
-java-testing-utils.dir:
+java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir
 	$(MAKE) $(MAKEARGS) -C java-testing-utils
 
+java-testing-utils-clean:
+	$(MAKE) $(MAKEARGS) -C java-testing-utils clean
+
 # We need to link bmc.o to the unit test, so here's everything it depends on...
 BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
@@ -118,16 +138,25 @@ OBJ += $(CPROVER_LIBS) \
        $(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \
        java-testing-utils/java-testing-utils$(LIBEXT)
 
-TESTS = unit_tests$(EXEEXT) \
-        # Empty last line
+CATCH_TEST = unit_tests$(EXEEXT)
+N_CATCH_TESTS = $(shell \
+                  cat $$(find . -name "*.cpp" ) | \
+                  grep -c -E "(SCENARIO|TEST_CASE)")
+
+CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT)
+
+# only add a dependency for libraries to avoid triggering implicit rules, which
+# would cause unnecessary rebuilds
+$(filter %$(LIBEXT), CPROVER_LIBS): jprover.dir
 
-CLEANFILES = $(TESTS)
+all: $(CATCH_TEST)
 
-all: cprover.dir cprover-testing-utils.dir jprover.dir java-testing-utils.dir
-	$(MAKE) $(MAKEARGS) $(TESTS)
+clean: java-testing-utils-clean
 
-test: all
-	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
+test: $(CATCH_TEST)
+	if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \
+	  ./$(CATCH_TEST) -l ; fi
+	./$(CATCH_TEST)
 
 
 ###############################################################################

jbmc/unit/java_bytecode/expr2java.cpp

@@ -96,21 +96,37 @@ TEST_CASE(
   SECTION("Hex float to string (print a comment)")
   {
     const float value = std::strtod("0x1p+37f", nullptr);
+#ifndef _MSC_VER
     REQUIRE(
       floating_point_to_java_string(value) == "0x1p+37f /* 1.37439e+11 */");
+#else
+    REQUIRE(
+      floating_point_to_java_string(value) ==
+      "0x1.000000p+37f /* 1.37439e+11 */");
+#endif
   }
 
   SECTION("Hex double to string (print a comment)")
   {
     const double value = std::strtod("0x1p+37f", nullptr);
+#ifndef _MSC_VER
     REQUIRE(
       floating_point_to_java_string(value) == "0x1p+37 /* 1.37439e+11 */");
+#else
+    REQUIRE(
+      floating_point_to_java_string(value) ==
+      "0x1.000000p+37 /* 1.37439e+11 */");
+#endif
   }
 
   SECTION("Beyond numeric limits")
   {
+#ifndef _MSC_VER
     REQUIRE(
       floating_point_to_java_string(-5.56268e-309)
         .find("/* -5.56268e-309 */") != std::string::npos);
+#else
+    REQUIRE(floating_point_to_java_string(-5.56268e-309) == "-5.56268e-309");
+#endif
   }
 }

src/ansi-c/Makefile

@@ -115,8 +115,6 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c
 %.inc: %.h file_converter$(EXEEXT)
 	./file_converter$(EXEEXT) < $< > $@
 
-cprover_library.cpp: cprover_library.inc
-
 ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES)
 
 generated_files: \

src/cpp/Makefile

@@ -59,6 +59,11 @@ all: cpp$(LIBEXT)
 
 ###############################################################################
 
+# extra dependencies
+cprover_library$(OBJEXT): cprover_library.inc
+
+###############################################################################
+
 ../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp
 	$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
 
@@ -69,8 +74,6 @@ library_check: library/*.c
 cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c
 	cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@
 
-cprover_library.cpp: cprover_library.inc
-
 generated_files: cprover_library.inc
 
 ###############################################################################

src/util/format_expr.cpp

@@ -88,7 +88,7 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
     if(first)
       first = false;
     else
-      os << ' ' << src.id() << ' ';
+      os << ' ' << operator_str << ' ';
 
     const bool need_parentheses = bracket_subexpression(op, src);
 

unit/.gitignore

@@ -1,4 +1,3 @@
 # Unit test binaries
-miniBDD
 sharing_node
 unit_tests

unit/CMakeLists.txt

@@ -3,9 +3,6 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
 
 list(REMOVE_ITEM sources
-    # Used in executables
-    ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
-
     # Don't build
     ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
@@ -48,14 +45,3 @@ add_test(
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
 set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC")
-
-add_executable(miniBDD miniBDD.cpp)
-target_include_directories(miniBDD
-    PUBLIC
-    ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
-    ${CMAKE_CURRENT_SOURCE_DIR}
-)
-target_link_libraries(miniBDD solvers ansi-c)
-add_test(NAME miniBDD COMMAND $<TARGET_FILE:miniBDD>)
-set_tests_properties(miniBDD PROPERTIES LABELS "CORE;CBMC")

unit/Makefile

@@ -1,33 +1,36 @@
-.PHONY: all cprover.dir testing-utils.dir test
+.PHONY: all cprover.dir test testing-utils-clean
 
 # Source files for test utilities
 SRC = unit_tests.cpp \
-      catch_example.cpp \
       # Empty last line
 
 # Test source files
-SRC += unit_tests.cpp \
-       analyses/ai/ai.cpp \
+SRC += analyses/ai/ai.cpp \
        analyses/ai/ai_simplify_lhs.cpp \
        analyses/call_graph.cpp \
        analyses/constant_propagator.cpp \
+       analyses/dependence_graph.cpp \
        analyses/disconnect_unreachable_nodes_in_graph.cpp \
        analyses/does_remove_const/does_expr_lose_const.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 \
+       interpreter/interpreter.cpp \
+       json/json_parser.cpp \
        path_strategies.cpp \
+       pointer-analysis/value_set.cpp \
        solvers/floatbv/float_utils.cpp \
+       solvers/miniBDD/miniBDD.cpp \
        solvers/refinement/array_pool/array_pool.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_refinement/concretize_array.cpp \
-       solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/sparse_array.cpp \
+       solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
-       util/expr.cpp \
        util/expr_cast/expr_cast.cpp \
+       util/expr.cpp \
        util/file_util.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \
@@ -36,16 +39,14 @@ SRC += unit_tests.cpp \
        util/message.cpp \
        util/optional.cpp \
        util/replace_symbol.cpp \
-       util/sharing_node.cpp \
        util/sharing_map.cpp \
+       util/sharing_node.cpp \
        util/small_map.cpp \
        util/small_shared_two_way_ptr.cpp \
        util/string_utils/split_string.cpp \
        util/string_utils/strip_string.cpp \
        util/symbol_table.cpp \
        util/unicode.cpp \
-       catch_example.cpp \
-       interpreter/interpreter.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.
@@ -56,9 +57,12 @@ include ../src/common
 cprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src
 
-testing-utils.dir:
+testing-utils/testing-utils$(LIBEXT): cprover.dir
 	$(MAKE) $(MAKEARGS) -C testing-utils
 
+testing-utils-clean:
+	$(MAKE) $(MAKEARGS) -C testing-utils clean
+
 # 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) \
@@ -107,23 +111,29 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \
 
 OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT)
 
-TESTS = unit_tests$(EXEEXT) \
-        miniBDD$(EXEEXT) \
-        # Empty last line
+CATCH_TEST = unit_tests$(EXEEXT)
+N_CATCH_TESTS = $(shell \
+                  cat $$(find . -name "*.cpp" \
+                    -a -not -name "expr_undefined_casts.cpp") | \
+                  grep -c -E "(SCENARIO|TEST_CASE)")
+
+CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT)
 
-CLEANFILES = $(TESTS)
+# only add a dependency for libraries to avoid triggering implicit rules, which
+# would cause unnecessary rebuilds
+$(filter %$(LIBEXT), CPROVER_LIBS): cprover.dir
 
-all: cprover.dir testing-utils.dir
-	$(MAKE) $(MAKEARGS) $(TESTS)
+all: $(CATCH_TEST)
 
-test: all
-	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
+clean: testing-utils-clean
+
+test: $(CATCH_TEST)
+	if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \
+		./$(CATCH_TEST) -l ; fi
+	./$(CATCH_TEST)
 
 
 ###############################################################################
 
 unit_tests$(EXEEXT): $(OBJ)
 	$(LINKBIN)
-
-miniBDD$(EXEEXT): miniBDD$(OBJEXT) $(CPROVER_LIBS)
-	$(LINKBIN)