test(exception): add new tests exception and parser_exception

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

src/tests/util/CMakeLists.txt

@@ -43,3 +43,6 @@ 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)
+add_executable(exception exception.cpp)
+target_link_libraries(exception ${EXTRA_LIBS})
+add_test(exception ${CMAKE_CURRENT_BINARY_DIR}/exception)

src/tests/util/exception.cpp

@@ -0,0 +1,42 @@
+/*
+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 "util/test.h"
+#include "util/exception.h"
+#include "util/sstream.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"), 10, 100);
+    } catch (parser_exception & ex) {
+        lean_assert(std::string("(line: 10, pos: 100) foo") == ex.what());
+    }
+}
+
+static void tst3() {
+    try {
+        throw parser_exception(sstream() << "msg " << 10 << " " << 20, 10, 100);
+    } catch (parser_exception & ex) {
+        lean_assert(std::string("(line: 10, pos: 100) msg 10 20") == ex.what());
+    }
+}
+
+int main() {
+    tst1();
+    tst2();
+    tst3();
+    return has_violations() ? 1 : 0;
+}

src/util/exception.cpp

@@ -10,18 +10,15 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 
 namespace lean {
-
 exception::exception(char const * msg):m_msg(msg) {}
 exception::exception(std::string const & msg):m_msg(msg) {}
 exception::exception(sstream const & strm):m_msg(strm.str()) {}
-exception::exception(exception const & e):m_msg(e.m_msg) {}
 exception::~exception() noexcept {}
 char const * exception::what() const noexcept { return m_msg.c_str(); }
 
 parser_exception::parser_exception(char const * msg, unsigned l, unsigned p):exception(msg), m_line(l), m_pos(p) {}
 parser_exception::parser_exception(std::string const & msg, unsigned l, unsigned p):exception(msg), m_line(l), m_pos(p) {}
 parser_exception::parser_exception(sstream const & msg, unsigned l, unsigned p):exception(msg), m_line(l), m_pos(p) {}
-parser_exception::parser_exception(parser_exception const & e):exception(e), m_line(e.m_line), m_pos(e.m_pos) {}
 parser_exception::~parser_exception() noexcept {}
 char const * parser_exception::what() const noexcept {
     try {

src/util/exception.h

@@ -19,7 +19,6 @@ public:
     exception(char const * msg);
     exception(std::string const & msg);
     exception(sstream const & strm);
-    exception(exception const & ex);
     virtual ~exception() noexcept;
     virtual char const * what() const noexcept;
 };
@@ -32,7 +31,6 @@ public:
     parser_exception(char const * msg, unsigned l, unsigned p);
     parser_exception(std::string const & msg, unsigned l, unsigned p);
     parser_exception(sstream const & strm, unsigned l, unsigned p);
-    parser_exception(parser_exception const & ex);
     virtual ~parser_exception() noexcept;
     virtual char const * what() const noexcept;
     unsigned get_line() const { return m_line; }