From 87e749cd123b2d70a580ad663bc7a61682678ec9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Sep 2013 20:30:05 -0700 Subject: [PATCH] test(trace): add unit test for trace module Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 3 +++ src/tests/util/trace.cpp | 18 ++++++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 src/tests/util/trace.cpp diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index fe9af0c9f..6154db36a 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -40,3 +40,6 @@ add_test(splay_tree ${CMAKE_CURRENT_BINARY_DIR}/splay_tree) add_executable(splay_map splay_map.cpp) target_link_libraries(splay_map ${EXTRA_LIBS}) add_test(splay_map ${CMAKE_CURRENT_BINARY_DIR}/splay_map) +add_executable(trace trace.cpp) +target_link_libraries(trace ${EXTRA_LIBS}) +add_test(trace ${CMAKE_CURRENT_BINARY_DIR}/trace) diff --git a/src/tests/util/trace.cpp b/src/tests/util/trace.cpp new file mode 100644 index 000000000..445733050 --- /dev/null +++ b/src/tests/util/trace.cpp @@ -0,0 +1,18 @@ +/* +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 "util/test.h" +#include "util/trace.h" +using namespace lean; + +int main() { + lean_assert(!is_trace_enabled("name")); + enable_trace("name"); + lean_assert(is_trace_enabled("name")); + disable_trace("name"); + lean_assert(!is_trace_enabled("name")); + return has_violations() ? 1 : 0; +}