diffblue · thk123 · Oct 10, 2017 · Oct 9, 2017
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
@@ -3,6 +3,9 @@ set(CMAKE_CXX_STANDARD_REQUIRED true)
 
 file(GLOB_RECURSE sources "*.cpp")
 file(GLOB_RECURSE headers "*.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
@@ -22,18 +25,23 @@ list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
 
+    # Will be built into a separate library and linked
+    ${testing_utils}
+
     # Intended to fail to compile
     ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
 )
 
+add_subdirectory(testing-utils)
+
 add_executable(unit ${sources} ${headers})
 target_include_directories(unit
     PUBLIC
     ${CBMC_BINARY_DIR}
     ${CBMC_SOURCE_DIR}
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
-target_link_libraries(unit ansi-c solvers java_bytecode)
+target_link_libraries(unit testing-utils ansi-c solvers java_bytecode)
 add_test(
     NAME unit
     COMMAND $<TARGET_FILE:unit>

diff --git a/unit/Makefile b/unit/Makefile
@@ -1,10 +1,7 @@
 .PHONY: all cprover.dir test
 
 # Source files for test utilities
-SRC = src/expr/require_expr.cpp \
-      src/ansi-c/c_to_expr.cpp \
-      src/java_bytecode/load_java_class.cpp \
-      unit_tests.cpp \
+SRC = unit_tests.cpp \
       catch_example.cpp \
       util/expr_iterator.cpp \
       util/optional.cpp \
@@ -42,6 +39,9 @@ include ../src/common
 cprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src
 
+testing-utils/testing-utils$(LIBEXT):
+	$(MAKE) $(MAKEARGS) -C testing-utils
+
 CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               ../src/miniz/miniz$(OBJEXT) \
               ../src/ansi-c/ansi-c$(LIBEXT) \
@@ -58,7 +58,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               ../src/solvers/solvers$(LIBEXT) \
               # Empty last line
 
-OBJ += $(CPROVER_LIBS)
+OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT)
 
 TESTS = unit_tests$(EXEEXT) \
         miniBDD$(EXEEXT) \

diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp
@@ -9,7 +9,7 @@
 /// \file
 /// Unit tests for ai_domain_baset::ai_simplify_lhs
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <analyses/ai.h>
 

diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp
@@ -8,7 +8,7 @@ Module: Unit test for call graph generation
 
 #include <iostream>
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <analyses/call_graph.h>
 

diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp
@@ -9,7 +9,7 @@
 /// \file
 /// Does Remove Const Unit Tests
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <util/std_expr.h>
 #include <util/std_code.h>

diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp
@@ -9,7 +9,7 @@
 /// \file
 /// Does Remove Const Unit Tests
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <util/c_types.h>
 #include <util/namespace.h>

diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp
@@ -9,7 +9,7 @@
 /// \file
 /// Does Remove Const Unit Tests
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <util/c_types.h>
 #include <util/namespace.h>

diff --git a/unit/catch_example.cpp b/unit/catch_example.cpp
@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 unsigned int Factorial(unsigned int number)
 {

diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp
@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <istream>
 #include <memory>
@@ -15,7 +15,7 @@
 #include <util/language.h>
 #include <util/message.h>
 #include <java_bytecode/java_bytecode_language.h>
-#include <src/java_bytecode/load_java_class.h>
+#include <testing-utils/load_java_class.h>
 
 SCENARIO("java_bytecode_convert_abstract_class",
   "[core][java_bytecode][java_bytecode_convert_class]")

diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -7,7 +7,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 #include <util/c_types.h>
 #include <util/expr.h>
 #include <util/std_code.h>

diff --git a/unit/miniBDD_new.cpp b/unit/miniBDD_new.cpp
@@ -9,7 +9,7 @@
 /// \file
 /// Unit tests for miniBDD
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <solvers/miniBDD/miniBDD.h>
 #include <solvers/flattening/boolbv.h>

diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp
@@ -7,7 +7,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <solvers/refinement/string_constraint_generator.h>
 #include <util/std_types.h>

diff --git a/...lvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/...lvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
@@ -7,7 +7,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <solvers/refinement/string_constraint_generator.h>
 #include <util/namespace.h>

diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp
@@ -7,7 +7,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <solvers/refinement/string_constraint_generator.h>
 #include <util/namespace.h>

diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <solvers/refinement/string_constraint_instantiation.h>
 

diff --git a/unit/solvers/refinement/string_refinement/concretize_array.cpp b/unit/solvers/refinement/string_refinement/concretize_array.cpp
@@ -7,7 +7,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <util/arith_tools.h>
 #include <util/std_types.h>

diff --git a/unit/solvers/refinement/string_refinement/substitute_array_list.cpp b/unit/solvers/refinement/string_refinement/substitute_array_list.cpp
@@ -7,7 +7,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <util/arith_tools.h>
 #include <util/std_types.h>

diff --git a/unit/testing-utils/CMakeLists.txt b/unit/testing-utils/CMakeLists.txt
@@ -0,0 +1,10 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(testing-utils ${sources})
+target_link_libraries(testing-utils
+    util
+    java_bytecode
+)
+target_include_directories(testing-utils
+    PUBLIC
+    ${CMAKE_CURRENT_SOURCE_DIR}/..
+)
diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile
@@ -0,0 +1,18 @@
+SRC = \
+  c_to_expr.cpp \
+  load_java_class.cpp \
+  require_expr.cpp \
+  # Empty last line (please keep above list sorted!)
+
+INCLUDES = -I .. -I . -I ../../src
+
+include ../../src/config.inc
+include ../../src/common
+
+CLEANFILES = testing-utils$(LIBEXT)
+
+.PHONY: all
+all: testing-utils$(LIBEXT)
+
+testing-utils$(LIBEXT): $(OBJ)
+	$(LINKLIB)
diff --git a/unit/src/ansi-c/c_to_expr.cpp → unit/testing-utils/c_to_expr.cpp b/unit/src/ansi-c/c_to_expr.cpp → unit/testing-utils/c_to_expr.cpp
@@ -12,7 +12,7 @@
 ///
 #include "c_to_expr.h"
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 c_to_exprt::c_to_exprt():
   message_handler(

diff --git a/unit/src/ansi-c/c_to_expr.h → unit/testing-utils/c_to_expr.h b/unit/src/ansi-c/c_to_expr.h → unit/testing-utils/c_to_expr.h
@@ -10,8 +10,8 @@
 /// Utility for converting strings in to exprt, throwing a CATCH exception
 /// if this fails in any way.
 
-#ifndef CPROVER_SRC_ANSI_C_C_TO_EXPR_H
-#define CPROVER_SRC_ANSI_C_C_TO_EXPR_H
+#ifndef CPROVER_TESTING_UTILS_C_TO_EXPR_H
+#define CPROVER_TESTING_UTILS_C_TO_EXPR_H
 
 #include <memory>
 
@@ -32,4 +32,4 @@ class c_to_exprt
   ansi_c_languaget language;
 };
 
-#endif // CPROVER_SRC_ANSI_C_C_TO_EXPR_H
+#endif // CPROVER_TESTING_UTILS_C_TO_EXPR_H
diff --git a/unit/catch.hpp → unit/testing-utils/catch.hpp b/unit/catch.hpp → unit/testing-utils/catch.hpp
diff --git a/unit/src/java_bytecode/load_java_class.cpp → unit/testing-utils/load_java_class.cpp b/unit/src/java_bytecode/load_java_class.cpp → unit/testing-utils/load_java_class.cpp
@@ -7,7 +7,7 @@
 \*******************************************************************/
 
 #include "load_java_class.h"
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 #include <iostream>
 
 #include <util/config.h>

diff --git a/unit/src/java_bytecode/load_java_class.h → unit/testing-utils/load_java_class.h b/unit/src/java_bytecode/load_java_class.h → unit/testing-utils/load_java_class.h
@@ -10,13 +10,13 @@
 /// Utility for loading and parsing a specified java class file, returning
 /// the symbol table generated by this.
 
-#ifndef CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H
-#define CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H
+#ifndef CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H
+#define CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H
 
 #include <util/symbol_table.h>
 
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path);
 
-#endif // CPROVER_SRC_JAVA_BYTECODE_LOAD_JAVA_CLASS_H
+#endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H
diff --git a/unit/src/expr/require_expr.cpp → unit/testing-utils/require_expr.cpp b/unit/src/expr/require_expr.cpp → unit/testing-utils/require_expr.cpp
@@ -14,7 +14,7 @@
 
 #include "require_expr.h"
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 #include <util/arith_tools.h>
 
 /// Verify a given exprt is an index_exprt with a a constant value equal to the

diff --git a/unit/src/expr/require_expr.h → unit/testing-utils/require_expr.h b/unit/src/expr/require_expr.h → unit/testing-utils/require_expr.h
@@ -12,8 +12,8 @@
 /// Also checks associated properties and returns a casted version of the
 /// expression.
 
-#ifndef CPROVER_SRC_EXPR_REQUIRE_EXPR_H
-#define CPROVER_SRC_EXPR_REQUIRE_EXPR_H
+#ifndef CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
+#define CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
 
 #include <util/std_expr.h>
 
@@ -30,4 +30,4 @@ namespace require_expr
     const exprt &expr, const irep_idt &symbol_name);
 }
 
-#endif // CPROVER_SRC_EXPR_REQUIRE_EXPR_H
+#endif // CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
diff --git a/unit/unit_tests.cpp b/unit/unit_tests.cpp
@@ -7,7 +7,7 @@
 \*******************************************************************/
 
 #define CATCH_CONFIG_MAIN
-#include "catch.hpp"
+#include <testing-utils/catch.hpp>
 #include <util/irep.h>
 
 // Debug printer for irept

diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
@@ -5,7 +5,7 @@
 /// \file
 /// expr_dynamic_cast Unit Tests
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/std_types.h>

diff --git a/unit/util/expr_iterator.cpp b/unit/util/expr_iterator.cpp
@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 #include <util/expr.h>
 #include <util/expr_iterator.h>
 

diff --git a/unit/util/optional.cpp b/unit/util/optional.cpp
@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include "catch.hpp"
+#include <testing-utils/catch.hpp>
 #include <util/optional.h>
 
 TEST_CASE("Optional without a value", "[core][util][optional]")

diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <java_bytecode/java_types.h>
 #include <util/arith_tools.h>