max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/util): remove exception test

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-07 14:06:34 -07:00
parent 2d7b6ed12c
commit c697cf4c29
2 changed files with 0 additions and 98 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -22,9 +22,6 @@ add_exec_test(rb_tree "rb_tree")
add_executable(rb_map rb_map.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(rb_map ${EXTRA_LIBS})
add_exec_test(rb_map "rb_map")
add_executable(exception exception.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(exception ${EXTRA_LIBS})
add_exec_test(exception "exception")
add_executable(bit_tricks bit_tricks.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(bit_tricks ${EXTRA_LIBS})
add_exec_test(bit_tricks "bit_tricks")

95
src/tests/util/exception.cpp
View file

@ -1,95 +0,0 @@
/*
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 <string>
#include <functional>
#include "runtime/sstream.h"
#include "util/test.h"
#include "util/parser_exception.h"
#include "util/init_module.h"
using namespace lean;
static void tst1() {
try {
throw exception(std::string("foo"));
} catch (exception & ex) {
lean_assert(std::string("foo") == ex.what());
}
}
static void tst2() {
try {
throw parser_exception(std::string("foo"), "[string]", {10, 100});
} catch (parser_exception & ex) {
lean_assert(std::string("[string]:10:100: error: foo") == ex.what());
}
}
static void tst3() {
try {
throw parser_exception(sstream() << "msg " << 10 << " " << 20, "[stream]", {10, 100});
} catch (parser_exception & ex) {
lean_assert(std::string("[stream]:10:100: error: msg 10 20") == ex.what());
}
}
static void tst4() {
try {
throw interrupted();
} catch (interrupted & ex) {
lean_assert(std::string("interrupted") == ex.what());
}
}
class ex : public exception {
std::function<char const *()> m_f;
public:
ex(std::function<char const *()> const & f):m_f(f) {}
virtual throwable * clone() const { return new ex(m_f); }
virtual void rethrow() const { throw *this; }
virtual char const * what() const noexcept { return m_f(); }
};
static void throw_ex() {
int x = 10;
std::string msg = "foo";
throw ex([=]() {
static std::string m;
std::ostringstream buffer;
buffer << "error, x: " << x << " " << msg;
m = buffer.str();
return m.c_str();
});
}
static void throw_catch_rethrow() {
try {
throw_ex();
} catch (ex & e) {
std::cout << "CATCH 1: {" << e.what() << "}\n";
std::unique_ptr<throwable> new_e(e.clone());
new_e->rethrow();
}
}
static void tst5() {
try {
throw_catch_rethrow();
} catch (ex & e) {
std::cout << "CATCH 2: {" << e.what() << "}\n";
}
}
int main() {
initialize_util_module();
tst1();
tst2();
tst3();
tst4();
tst5();
finalize_util_module();
return has_violations() ? 1 : 0;
}