Add basic testing infrastructure using CTest

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/CMakeLists.txt

@@ -4,6 +4,7 @@ set (LEAN_VERSION_MAJOR 0)
 set(LEAN_VERSION_MINOR 1)
 
 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)
 

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)

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

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

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 <iostream>
+#include "test.h"
+#include "mpq.h"
+
+int main() {
+    lean::abort_on_violation(true);
+    lean_assert(false);
+    std::cout << "PASSED\n";
+    return 0;
+}

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<std::set<std::string>> 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

src/util/debug.h

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 
 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);

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"
+