From: Aina Niemetz Date: Tue, 2 Mar 2021 22:06:38 +0000 (-0800) Subject: Remove obsolete dependency on CxxTest. (#6038) X-Git-Tag: cvc5-1.0.0~2169 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=32699ab8393f4d3cb02c9a132ea174c7a1e5e958;p=cvc5.git Remove obsolete dependency on CxxTest. (#6038) --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index abd47ec97..eb95a7bef 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -64,7 +64,6 @@ jobs: sudo apt-get install -y \ build-essential \ ccache \ - cxxtest \ libcln-dev \ libgmp-dev \ libgtest-dev \ @@ -87,7 +86,6 @@ jobs: run: | brew install \ ccache \ - cxxtest \ cln \ gmp \ pkgconfig \ diff --git a/CMakeLists.txt b/CMakeLists.txt index b48974cc3..060753864 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -68,9 +68,6 @@ endif() if(CRYPTOMINISAT_DIR) list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}") endif() -if(CXXTEST_DIR) - list(APPEND CMAKE_PREFIX_PATH "${CXXTEST_DIR}") -endif() if(DRAT2ER_DIR) list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}") endif() @@ -164,7 +161,6 @@ set(ABC_DIR "" CACHE STRING "Set ABC install directory") set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory") set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory") set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory") -set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory") set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") set(GMP_DIR "" CACHE STRING "Set GMP install directory") diff --git a/INSTALL.md b/INSTALL.md index fc19dc946..635118f1d 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -189,13 +189,6 @@ for a package named "libedit-dev" or "libedit-devel" or similar. The [Boost](http://www.boost.org) C++ base library is needed for some examples provided with CVC4. -### CxxTest Unit Testing Framework (Unit Tests) - -[CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests -(included with the distribution). -See [Testing CVC4](#Testing-CVC4) below for more details. - - ### Google Test Unit Testing Framework (Unit Tests) [Google Test](https://github.com/google/googletest) is required to optionally diff --git a/cmake/FindCxxTest.cmake b/cmake/FindCxxTest.cmake deleted file mode 100644 index f21a4fe0d..000000000 --- a/cmake/FindCxxTest.cmake +++ /dev/null @@ -1,60 +0,0 @@ -##################### -## FindCxxTest.cmake -## Top contributors (to current version): -## Mathias Preiner, Alex Ozdemir, Andrew Reynolds -## This file is part of the CVC4 project. -## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -# Find CxxTest -# CxxTest_FOUND - system has CxxTest lib -# CxxTest_INCLUDE_DIR - the CxxTest include directory -# CxxTest_TESTGEN_EXECUTABLE - CxxTest excecutable -# CxxTest_TESTGEN_INTERPRETER - Python/Perl interpreter for running executable - -find_package(PythonInterp QUIET) -find_package(Perl QUIET) - -find_path(CxxTest_INCLUDE_DIR cxxtest/TestSuite.h - PATHS ${CxxTest_HOME} - NO_DEFAULT_PATH) -find_program(CxxTest_PYTHON_TESTGEN_EXECUTABLE - NAMES cxxtestgen cxxtestgen.py - PATHS ${CxxTest_HOME}/bin - NO_DEFAULT_PATH) -find_program(CxxTest_PERL_TESTGEN_EXECUTABLE cxxtestgen.pl - PATHS ${CxxTest_HOME}/bin - NO_DEFAULT_PATH) - -if(NOT CxxTest_HOME) - find_path(CxxTest_INCLUDE_DIR cxxtest/TestSuite.h) - find_program(CxxTest_PYTHON_TESTGEN_EXECUTABLE NAMES cxxtestgen.py) - find_program(CxxTest_SHEBANG_TESTGEN_EXECUTABLE NAMES cxxtestgen) - find_program(CxxTest_PERL_TESTGEN_EXECUTABLE cxxtestgen.pl) -endif() - - -if(CxxTest_SHEBANG_TESTGEN_EXECUTABLE) - set(CxxTest_USE_SHEBANG ON) - set(CxxTest_TESTGEN_EXECUTABLE ${CxxTest_SHEBANG_TESTGEN_EXECUTABLE}) -elseif(PYTHONINTERP_FOUND AND CxxTest_PYTHON_TESTGEN_EXECUTABLE) - set(CxxTest_TESTGEN_EXECUTABLE ${CxxTest_PYTHON_TESTGEN_EXECUTABLE}) - set(CxxTest_TESTGEN_INTERPRETER ${PYTHON_EXECUTABLE}) -elseif(PERL_FOUND AND CxxTest_PERL_TESTGEN_EXECUTABLE) - set(CxxTest_TESTGEN_EXECUTABLE ${CxxTest_PERL_TESTGEN_EXECUTABLE}) - set(CxxTest_TESTGEN_INTERPRETER ${PERL_EXECUTABLE}) -elseif(NOT PYTHONINTERP_FOUND AND NOT PERL_FOUND AND CxxTest_FIND_REQUIRED) - message(FATAL_ERROR "Neither Python nor Perl found, cannot use CxxTest.") -endif() - -if(NOT DEFINED CxxTest_TESTGEN_ARGS) - set(CxxTest_TESTGEN_ARGS --error-printer) -endif() - -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args( - CxxTest DEFAULT_MSG CxxTest_INCLUDE_DIR CxxTest_TESTGEN_EXECUTABLE) - -mark_as_advanced(CxxTest_INCLUDE_DIR CxxTest_TESTGEN_EXECUTABLE) diff --git a/configure.sh b/configure.sh index e7a858486..f583b008a 100755 --- a/configure.sh +++ b/configure.sh @@ -74,7 +74,6 @@ Optional Path to Optional Packages: --cadical-dir=PATH path to top level of CaDiCaL source tree --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree --drat2er-dir=PATH path to the top level of the drat2er installation - --cxxtest-dir=PATH path to CxxTest installation --glpk-dir=PATH path to top level of GLPK installation --gmp-dir=PATH path to top level of GMP installation --kissat-dir=PATH path to top level of Kissat source tree @@ -160,7 +159,6 @@ antlr_dir=default cadical_dir=default cryptominisat_dir=default drat2er_dir=default -cxxtest_dir=default glpk_dir=default gmp_dir=default kissat_dir=default @@ -319,9 +317,6 @@ do --cryptominisat-dir) die "missing argument to $1 (try -h)" ;; --cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;; - --cxxtest-dir) die "missing argument to $1 (try -h)" ;; - --cxxtest-dir=*) cxxtest_dir=${1##*=} ;; - --drat2er-dir) die "missing argument to $1 (try -h)" ;; --drat2er-dir=*) drat2er_dir=${1##*=} ;; @@ -469,8 +464,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir" [ "$cryptominisat_dir" != default ] \ && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir" -[ "$cxxtest_dir" != default ] \ - && cmake_opts="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir" [ "$drat2er_dir" != default ] \ && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir" [ "$glpk_dir" != default ] \ diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 46ff346e0..fda403e84 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -8,11 +8,6 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -# Note: We use our custom CxxTest finder here to specify custom directories and -# fail if it is not found in the specified directory (similar to the other -# custom finder modules). -set(CxxTest_HOME ${CXXTEST_DIR}) -find_package(CxxTest REQUIRED) find_package(GTest REQUIRED) include(GoogleTest) @@ -35,7 +30,6 @@ add_custom_target(units set(CVC4_UNIT_TEST_FLAGS_BLACK -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) -set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_UNIT_TEST_FLAGS_BLACK}) # Generate and add unit test. macro(cvc4_add_unit_test is_white name output_dir) @@ -80,84 +74,6 @@ macro(cvc4_add_unit_test is_white name output_dir) set_tests_properties(${test_name} PROPERTIES LABELS "unit") endmacro() -# Generate and add unit test. -# Note: we do not use cxxtest_add_test from the FindCxxTest module since it -# does not allow test names containing '/'. -# !! This macro will be removed when all unit tests are migrated to Google Test. -macro(cvc4_add_cxx_unit_test is_white name output_dir) - # generate the test sources - set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp) - set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h) - if (CxxTest_USE_SHEBANG) - add_custom_command( - OUTPUT ${test_src} - DEPENDS ${test_header} - COMMAND - ${CxxTest_TESTGEN_EXECUTABLE} - ${CxxTest_TESTGEN_ARGS} -o ${test_src} ${test_header} - ) - else() - add_custom_command( - OUTPUT ${test_src} - DEPENDS ${test_header} - COMMAND - ${CxxTest_TESTGEN_INTERPRETER} - ${CxxTest_TESTGEN_EXECUTABLE} - ${CxxTest_TESTGEN_ARGS} -o ${test_src} ${test_header} - ) - endif() - set_source_files_properties(${test_src} PROPERTIES GENERATED true) - # The build target is created without the path prefix (not supported), - # e.g., for '/myunittest.h' - # we generate '${CMAKE_BINAR_DIR}/test/unit//myunittest.cpp', - # create build target 'myunittest' - # and build it with 'make myunittest'. - # As a consequence, all build target names must be globally unique. - add_executable(${name} ${test_src} ${test_header}) - target_link_libraries(${name} main-test) - target_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR}) - target_compile_definitions(${name} PRIVATE ${CVC4_UNIT_TEST_FLAGS_BLACK}) - if(USE_LFSC) - # We don't link against LFSC, because CVC4 is already linked against it. - target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR}) - endif() - if(USE_POLY) - # We don't link against libpoly, because CVC4 is already linked against it. - target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) - endif() - if(${is_white}) - target_compile_options(${name} PRIVATE -fno-access-control) - endif() - # Disable the Wsuggest-override warnings for the unit tests. CxxTest generates - # code that does not properly add the override keyword to runTest(). - check_cxx_compiler_flag("-Wno-suggest-override" HAVE_FLAGWno_suggest_override) - if(HAVE_FLAGWno_suggest_override) - target_compile_options(${name} PRIVATE -Wno-suggest-override) - endif() - # Disable the Wunused-comparison warnings for the unit tests. - check_cxx_compiler_flag("-Wno-unused-comparison" HAVE_FLAGWno_unused_comparison) - if(HAVE_FLAGWno_unused_comparison) - target_compile_options(${name} PRIVATE -Wno-unused-comparison) - endif() - - add_dependencies(build-units ${name}) - # Generate into bin/test/unit/. - set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) - set_target_properties(${name} - PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) - # The test target is prefixed with test identifier 'unit/' and the path, - # e.g., for '/myunittest.h' - # we create test target 'unit//myunittest' - # and run it with 'ctest -R "example//myunittest"'. - if("${output_dir}" STREQUAL "") - set(test_name unit/${name}) - else() - set(test_name unit/${output_dir}/${name}) - endif() - add_test(${test_name} ${test_bin_dir}/${name}) - set_tests_properties(${test_name} PROPERTIES LABELS "unit") -endmacro() - macro(cvc4_add_unit_test_black name output_dir) cvc4_add_unit_test(FALSE ${name} ${output_dir}) endmacro() @@ -165,15 +81,6 @@ macro(cvc4_add_unit_test_white name output_dir) cvc4_add_unit_test(TRUE ${name} ${output_dir}) endmacro() -# !! Will be removed when all unit tests are migrated to Google Test. -macro(cvc4_add_cxx_unit_test_black name output_dir) - cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir}) -endmacro() -# !! Will be removed when all unit tests are migrated to Google Test. -macro(cvc4_add_cxx_unit_test_white name output_dir) - cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir}) -endmacro() - add_subdirectory(api) add_subdirectory(base) add_subdirectory(context) diff --git a/test/unit/expr/node_manager_black.cpp b/test/unit/expr/node_manager_black.cpp index 4b72f0418..d9a236a64 100644 --- a/test/unit/expr/node_manager_black.cpp +++ b/test/unit/expr/node_manager_black.cpp @@ -21,7 +21,6 @@ #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" #include "test_node.h" -#include "test_utils.h" #include "util/integer.h" #include "util/rational.h" diff --git a/test/unit/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp index 2897a5588..4ca26ba7b 100644 --- a/test/unit/expr/symbol_table_black.cpp +++ b/test/unit/expr/symbol_table_black.cpp @@ -14,8 +14,6 @@ ** Black box testing of CVC4::SymbolTable. **/ -#include - #include #include diff --git a/test/unit/test_utils.h b/test/unit/test_utils.h deleted file mode 100644 index 155d923ed..000000000 --- a/test/unit/test_utils.h +++ /dev/null @@ -1,37 +0,0 @@ -/********************* */ -/*! \file test_utils.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for testing. - ** - **/ - -#include -#include - -/** - * Use TS_UTILS_EXPECT_ABORT if you expect the expression to abort() when a - * AlwaysAssert or Assert is triggered. - */ -#define TS_UTILS_EXPECT_ABORT(expr) \ - do \ - { \ - int32_t status; \ - if (fork()) \ - { \ - wait(&status); \ - } \ - else \ - { \ - expr; \ - exit(EXIT_SUCCESS); \ - } \ - TS_ASSERT(WIFSIGNALED(status)); \ - } while (0) diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index a0a954008..74dace3fd 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -18,7 +18,6 @@ #include "expr/expr.h" #include "expr/type.h" #include "test_smt.h" -#include "test_utils.h" namespace CVC4 { namespace test {