michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(trace): add unit test for trace module

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-25 20:30:05 -07:00
parent e16f45854b
commit 87e749cd12
2 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/util/CMakeLists.txt
View file

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

18
src/tests/util/trace.cpp Normal file
View file

@ -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;
}