From e559bf73a913bc9b74cc81dd3fe3e810a7fadae2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Jul 2013 09:12:07 -0700 Subject: [PATCH] Add basic testing infrastructure using CTest Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 22 +++++++++++++--------- src/numerics/CMakeLists.txt | 1 - src/shell/CMakeLists.txt | 15 ++------------- src/tests/numerics/CMakeLists.txt | 4 ++++ src/tests/numerics/mpq.cpp | 16 ++++++++++++++++ src/util/debug.cpp | 9 ++++++++- src/util/debug.h | 3 ++- src/util/test.h | 13 +++++++++++++ 8 files changed, 58 insertions(+), 25 deletions(-) create mode 100644 src/tests/numerics/CMakeLists.txt create mode 100644 src/tests/numerics/mpq.cpp create mode 100644 src/util/test.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8f818e59b..36b652103 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,9 +1,10 @@ -cmake_minimum_required (VERSION 2.8.7) -project (LEAN CXX) -set (LEAN_VERSION_MAJOR 0) -set (LEAN_VERSION_MINOR 1) +cmake_minimum_required(VERSION 2.8.7) +project(LEAN CXX) +set(LEAN_VERSION_MAJOR 0) +set(LEAN_VERSION_MINOR 1) -set (CMAKE_COLOR_MAKEFILE ON) +set(CMAKE_COLOR_MAKEFILE ON) +enable_testing() # Initialize CXXFLAGS. set(CMAKE_CXX_FLAGS "-Wall -std=c++11") @@ -32,15 +33,18 @@ endif (GMP_INCLUDE_DIR AND GMP_LIBRARIES) find_path(GMP_INCLUDE_DIR NAMES gmp.h ) find_library(GMP_LIBRARIES NAMES gmp libgmp ) -MESSAGE(STATUS "GMP: " ${GMP_LIBRARIES}) +message(STATUS "GMP: " ${GMP_LIBRARIES}) include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) +find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES) -set (CMAKE_CXX_COMPILER clang++) - +include_directories(${LEAN_SOURCE_DIR}/util) +include_directories(${LEAN_SOURCE_DIR}/numerics) add_subdirectory(util) add_subdirectory(numerics) +set(EXTRA_LIBS ${EXTRA_LIBS} util numerics ${GMP_LIBRARIES}) +set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") add_subdirectory(shell) +add_subdirectory(tests/numerics) diff --git a/src/numerics/CMakeLists.txt b/src/numerics/CMakeLists.txt index 308a1ffb4..f7b25f130 100644 --- a/src/numerics/CMakeLists.txt +++ b/src/numerics/CMakeLists.txt @@ -1,2 +1 @@ -include_directories (${LEAN_SOURCE_DIR}/util) add_library(numerics gmp_init.cpp mpz.cpp mpq.cpp mpbq.cpp) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index ef939789e..0a456c9b4 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -1,15 +1,4 @@ -configure_file ( - "${LEAN_SOURCE_DIR}/shell/version.h.in" - "${LEAN_BINARY_DIR}/version.h" - ) - +configure_file("${LEAN_SOURCE_DIR}/shell/version.h.in" "${LEAN_BINARY_DIR}/version.h") include_directories("${LEAN_BINARY_DIR}") - -include_directories (${LEAN_SOURCE_DIR}/util) -include_directories (${LEAN_SOURCE_DIR}/numerics) -set (EXTRA_LIBS ${EXTRA_LIBS} util numerics ${GMP_LIBRARIES}) - -set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") - add_executable(lean lean.cpp) -target_link_libraries (lean ${EXTRA_LIBS}) +target_link_libraries(lean ${EXTRA_LIBS}) diff --git a/src/tests/numerics/CMakeLists.txt b/src/tests/numerics/CMakeLists.txt new file mode 100644 index 000000000..bb742045a --- /dev/null +++ b/src/tests/numerics/CMakeLists.txt @@ -0,0 +1,4 @@ +include_directories(${LEAN_SOURCE_DIR}/numerics) +add_executable(mpq mpq.cpp) +add_test(mpq ${CMAKE_CURRENT_BINARY_DIR}/mpq) +target_link_libraries(mpq ${EXTRA_LIBS}) diff --git a/src/tests/numerics/mpq.cpp b/src/tests/numerics/mpq.cpp new file mode 100644 index 000000000..f77e99e13 --- /dev/null +++ b/src/tests/numerics/mpq.cpp @@ -0,0 +1,16 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "test.h" +#include "mpq.h" + +int main() { + lean::abort_on_violation(true); + lean_assert(false); + std::cout << "PASSED\n"; + return 0; +} diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 9dd2c075e..879ce6cb1 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -19,9 +19,14 @@ Author: Leonardo de Moura namespace lean { -static volatile bool g_enable_assertions = true; +static bool g_abort_on_violation = false; +static bool g_enable_assertions = true; static std::unique_ptr> g_enabled_debug_tags; +void abort_on_violation(bool f) { + g_abort_on_violation = f; +} + void enable_assertions(bool f) { g_enable_assertions = f; } @@ -54,6 +59,8 @@ bool is_debug_enabled(const char * tag) { } void invoke_debugger() { + if (g_abort_on_violation) + exit(1); int * x = 0; for (;;) { #ifdef _WINDOWS diff --git a/src/util/debug.h b/src/util/debug.h index abe573369..fdcaa8e8b 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -32,7 +32,8 @@ Author: Leonardo de Moura #endif namespace lean { - + +void abort_on_violation(bool flag); void notify_assertion_violation(char const * file_name, int line, char const * condition); void enable_debug(char const * tag); void disable_debug(char const * tag); diff --git a/src/util/test.h b/src/util/test.h new file mode 100644 index 000000000..152c40209 --- /dev/null +++ b/src/util/test.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +// always define LEAN_DEBUG for unit-tests +#ifndef LEAN_DEBUG +#define LEAN_DEBUG +#endif +#include "debug.h" +