Add new testing-utils library

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,10 +25,15 @@ 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
@@ -33,7 +41,7 @@ target_include_directories(unit
     ${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>

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) \

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>
 

unit/analyses/call_graph.cpp

@@ -8,7 +8,7 @@ Author:
 
 #include <iostream>
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 #include <analyses/call_graph.h>
 

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>

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>

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>

unit/catch_example.cpp

@@ -6,7 +6,7 @@
 
 \*******************************************************************/
 
-#include <catch.hpp>
+#include <testing-utils/catch.hpp>
 
 unsigned int Factorial(unsigned int number)
 {

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]")

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>

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>

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>

unit/solvers/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>

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>

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>
 

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>

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>

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}/..
+)

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)

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(

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 @@ private:
   ansi_c_languaget language;
 };
 
-#endif // CPROVER_SRC_ANSI_C_C_TO_EXPR_H
+#endif // CPROVER_TESTING_UTILS_C_TO_EXPR_H

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>

unit/testing-utils/load_java_class.h

@@ -10,8 +10,8 @@
 /// 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>
 
@@ -19,4 +19,4 @@ 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

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

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

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

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>

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>
 

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]")

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>