Skip to content

Commit 7de9df8

Browse files
tautschnigtautschnig
authored
Merge pull request #2877 from tautschnig/jbmc-unit-tests
unit test Makefiles: add missing source files
2 parents 0e09f0c + bd55a28 commit 7de9df8

File tree

15 files changed

+179
-189
lines changed

15 files changed

+179
-189
lines changed

‎CMakeLists.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,6 @@ set_target_properties(
6868
json
6969
langapi
7070
linking
71-
miniBDD
7271
pointer-analysis
7372
solvers
7473
test-bigint

‎jbmc/regression/jbmc-generics/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ show:
2020
clean:
2121
find -name '*.out' -execdir $(RM) '{}' \;
2222
find -name '*.gb' -execdir $(RM) '{}' \;
23-
$(RM) tests.log
23+
$(RM) tests.log tests-symex-driven-loading.log
2424

2525
%.class: %.java ../../src/org.cprover.jar
2626
javac -g -cp ../../src/org.cprover.jar:. $<

‎jbmc/regression/strings-smoke-tests/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,4 +28,4 @@ show:
2828
clean:
2929
find -name '*.out' -execdir $(RM) '{}' \;
3030
find -name '*.gb' -execdir $(RM) '{}' \;
31-
$(RM) tests.log
31+
$(RM) tests.log tests-symex-driven-loading.log

‎jbmc/unit/Makefile

Lines changed: 50 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,53 @@
1-
.PHONY: all cprover.dir jprover.dir testing-utils.dir java-testing-utils.dir test
1+
.PHONY: all jprover.dir test java-testing-utils-clean
22

33
# Source files for test utilities
44
SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \
55
# Empty last line
66

77
# Test source files
8-
SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
8+
SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
9+
java_bytecode/expr2java.cpp \
10+
java_bytecode/goto_program_generics/generic_bases_test.cpp \
11+
java_bytecode/goto_program_generics/generic_parameters_test.cpp \
12+
java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \
913
java_bytecode/goto-programs/class_hierarchy_graph.cpp \
14+
java_bytecode/goto-programs/class_hierarchy_output.cpp \
1015
java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \
16+
java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
1117
java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
1218
java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
19+
java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \
1320
java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
21+
java_bytecode/java_bytecode_convert_method/convert_method.cpp \
22+
java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \
23+
java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \
24+
java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \
25+
java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp \
1426
java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
15-
java_bytecode/java_bytecode_parser/parse_java_class.cpp \
27+
java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp \
28+
java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp \
29+
java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp \
30+
java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp \
31+
java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
32+
java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp \
33+
java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \
34+
java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \
35+
java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \
36+
java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
37+
java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
38+
java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \
1639
java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
40+
java_bytecode/java_bytecode_parser/parse_java_class.cpp \
1741
java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
18-
java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
19-
java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
42+
java_bytecode/java_replace_nondet/replace_nondet.cpp \
2043
java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
2144
java_bytecode/java_types/erase_type_arguments.cpp \
2245
java_bytecode/java_types/generic_type_index.cpp \
2346
java_bytecode/java_types/java_generic_symbol_type.cpp \
2447
java_bytecode/java_types/java_type_from_string.cpp \
2548
java_bytecode/java_utils_test.cpp \
49+
java_bytecode/java_virtual_functions/virtual_functions.cpp \
2650
java_bytecode/load_method_by_regex.cpp \
27-
java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
2851
pointer-analysis/custom_value_set_analysis.cpp \
2952
solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
3053
solvers/refinement/string_refinement/dependency_graph.cpp \
@@ -33,9 +56,6 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
3356
util/has_subtype.cpp \
3457
util/parameter_indices.cpp \
3558
util/simplify_expr.cpp \
36-
java_bytecode/java_virtual_functions/virtual_functions.cpp \
37-
java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
38-
java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \
3959
# Empty last line
4060

4161
INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit
@@ -44,18 +64,18 @@ include ../src/config.inc
4464
include $(CPROVER_DIR)/src/config.inc
4565
include $(CPROVER_DIR)/src/common
4666

47-
cprover.dir:
48-
$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src
49-
5067
jprover.dir:
5168
$(MAKE) $(MAKEARGS) -C ../src
5269

53-
cprover-testing-utils.dir:
70+
$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT): jprover.dir
5471
$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils
5572

56-
java-testing-utils.dir:
73+
java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir
5774
$(MAKE) $(MAKEARGS) -C java-testing-utils
5875

76+
java-testing-utils-clean:
77+
$(MAKE) $(MAKEARGS) -C java-testing-utils clean
78+
5979
# We need to link bmc.o to the unit test, so here's everything it depends on...
6080
BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
6181
$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
@@ -118,16 +138,25 @@ OBJ += $(CPROVER_LIBS) \
118138
$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \
119139
java-testing-utils/java-testing-utils$(LIBEXT)
120140

121-
TESTS = unit_tests$(EXEEXT) \
122-
# Empty last line
141+
CATCH_TEST = unit_tests$(EXEEXT)
142+
N_CATCH_TESTS = $(shell \
143+
cat $$(find . -name "*.cpp" ) | \
144+
grep -c -E "(SCENARIO|TEST_CASE)")
145+
146+
CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT)
147+
148+
# only add a dependency for libraries to avoid triggering implicit rules, which
149+
# would cause unnecessary rebuilds
150+
$(filter %$(LIBEXT), CPROVER_LIBS): jprover.dir
123151

124-
CLEANFILES = $(TESTS)
152+
all: $(CATCH_TEST)
125153

126-
all: cprover.dir cprover-testing-utils.dir jprover.dir java-testing-utils.dir
127-
$(MAKE) $(MAKEARGS) $(TESTS)
154+
clean: java-testing-utils-clean
128155

129-
test: all
130-
$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
156+
test: $(CATCH_TEST)
157+
if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \
158+
./$(CATCH_TEST) -l ; fi
159+
./$(CATCH_TEST)
131160

132161

133162
###############################################################################

‎jbmc/unit/java_bytecode/expr2java.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,21 +96,37 @@ TEST_CASE(
9696
SECTION("Hex float to string (print a comment)")
9797
{
9898
const float value = std::strtod("0x1p+37f", nullptr);
99+
#ifndef _MSC_VER
99100
REQUIRE(
100101
floating_point_to_java_string(value) == "0x1p+37f /* 1.37439e+11 */");
102+
#else
103+
REQUIRE(
104+
floating_point_to_java_string(value) ==
105+
"0x1.000000p+37f /* 1.37439e+11 */");
106+
#endif
101107
}
102108

103109
SECTION("Hex double to string (print a comment)")
104110
{
105111
const double value = std::strtod("0x1p+37f", nullptr);
112+
#ifndef _MSC_VER
106113
REQUIRE(
107114
floating_point_to_java_string(value) == "0x1p+37 /* 1.37439e+11 */");
115+
#else
116+
REQUIRE(
117+
floating_point_to_java_string(value) ==
118+
"0x1.000000p+37 /* 1.37439e+11 */");
119+
#endif
108120
}
109121

110122
SECTION("Beyond numeric limits")
111123
{
124+
#ifndef _MSC_VER
112125
REQUIRE(
113126
floating_point_to_java_string(-5.56268e-309)
114127
.find("/* -5.56268e-309 */") != std::string::npos);
128+
#else
129+
REQUIRE(floating_point_to_java_string(-5.56268e-309) == "-5.56268e-309");
130+
#endif
115131
}
116132
}

‎src/ansi-c/Makefile

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -115,8 +115,6 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c
115115
%.inc: %.h file_converter$(EXEEXT)
116116
./file_converter$(EXEEXT) < $< > $@
117117

118-
cprover_library.cpp: cprover_library.inc
119-
120118
ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES)
121119

122120
generated_files: \

‎src/cpp/Makefile

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,11 @@ all: cpp$(LIBEXT)
5959

6060
###############################################################################
6161

62+
# extra dependencies
63+
cprover_library$(OBJEXT): cprover_library.inc
64+
65+
###############################################################################
66+
6267
../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp
6368
$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
6469

@@ -69,8 +74,6 @@ library_check: library/*.c
6974
cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c
7075
cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@
7176

72-
cprover_library.cpp: cprover_library.inc
73-
7477
generated_files: cprover_library.inc
7578

7679
###############################################################################

‎src/util/format_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
8888
if(first)
8989
first = false;
9090
else
91-
os << ' ' << src.id() << ' ';
91+
os << ' ' << operator_str << ' ';
9292

9393
const bool need_parentheses = bracket_subexpression(op, src);
9494

‎unit/.gitignore

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
11
# Unit test binaries
2-
miniBDD
32
sharing_node
43
unit_tests

‎unit/CMakeLists.txt

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,6 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
33
file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
44

55
list(REMOVE_ITEM sources
6-
# Used in executables
7-
${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
8-
96
# Don't build
107
${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
118
${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
@@ -48,14 +45,3 @@ add_test(
4845
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
4946
)
5047
set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC")
51-
52-
add_executable(miniBDD miniBDD.cpp)
53-
target_include_directories(miniBDD
54-
PUBLIC
55-
${CBMC_BINARY_DIR}
56-
${CBMC_SOURCE_DIR}
57-
${CMAKE_CURRENT_SOURCE_DIR}
58-
)
59-
target_link_libraries(miniBDD solvers ansi-c)
60-
add_test(NAME miniBDD COMMAND $<TARGET_FILE:miniBDD>)
61-
set_tests_properties(miniBDD PROPERTIES LABELS "CORE;CBMC")

0 commit comments

Comments
 (0)