From 15979ab991eb397aef38d86f4f1c732a8090a704 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Sep 2013 21:36:56 -0700 Subject: [PATCH] fix(lean): fix warnings produced by cppcheck Fix (relevant) warnings produced by http://cppcheck.sourceforge.net. Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 7 +------ src/frontends/lean/pp.cpp | 1 + src/tests/kernel/level.cpp | 4 ++-- src/tests/kernel/type_checker.cpp | 2 +- src/util/exception.cpp | 2 +- src/util/sexpr/format.cpp | 2 +- src/util/sexpr/format.h | 4 ++-- 7 files changed, 9 insertions(+), 13 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 554d3fec0..c11ba955b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -212,8 +212,6 @@ class parser::imp { bool curr_is_lcurly() const { return curr() == scanner::token::LeftCurlyBracket; } /** \brief Return true iff the current token is a ':' */ bool curr_is_colon() const { return curr() == scanner::token::Colon; } - /** \brief Return true iff the current token is a ',' */ - bool curr_is_comma() const { return curr() == scanner::token::Comma; } /** \brief Return true iff the current token is an 'in' token */ bool curr_is_in() const { return curr() == scanner::token::In; } @@ -230,8 +228,6 @@ class parser::imp { void check_colon_next(char const * msg) { check_next(scanner::token::Colon, msg); } /** \brief Throws a parser error if the current token is not ','. If it is, move to the next token. */ void check_comma_next(char const * msg) { check_next(scanner::token::Comma, msg); } - /** \brief Throws a parser error if the current token is not '('. If it is, move to the next token. */ - void check_lparen_next(char const * msg) { check_next(scanner::token::LeftParen, msg); } /** \brief Throws a parser error if the current token is not ')'. If it is, move to the next token. */ void check_rparen_next(char const * msg) { check_next(scanner::token::RightParen, msg); } /** \brief Throws a parser error if the current token is not '}'. If it is, move to the next token. */ @@ -1660,9 +1656,8 @@ shell::~shell() { bool shell::operator()() { #ifdef LEAN_USE_READLINE bool errors = false; - char * input; while (true) { - input = readline("# "); + char * input = readline("# "); if (!input) return errors; add_history(input); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e2177eb17..8447816f0 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1149,6 +1149,7 @@ public: m_frontend(fe) { set_options(opts); m_interrupted = false; + m_num_steps = 0; } format operator()(expr const & e) { diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index f1bc09a86..3b1af8e0d 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -46,7 +46,7 @@ static void tst2() { level l2 = env.add_uvar("l1", level()); lean_unreachable(); } - catch (exception ex) { + catch (exception & ex) { std::cout << "ok\n"; } } @@ -59,7 +59,7 @@ static void tst3() { level l3 = env.add_uvar("l3", l2 + (1<<30)); lean_unreachable(); } - catch (exception ex) { + catch (exception & ex) { std::cout << "ok\n"; } } diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 0f416ced2..76ce59511 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -69,7 +69,7 @@ static void tst2() { std::cout << F << "\n"; std::cout << infer_type(F, env) << "\n"; } - catch (exception ex) { + catch (exception & ex) { std::cout << "Error: " << ex.what() << "\n"; } } diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 49fece872..b3246351e 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -27,7 +27,7 @@ char const * parser_exception::what() const noexcept { s << "(line: " << m_line << ", pos: " << m_pos << ") " << m_msg; buffer = s.str(); return buffer.c_str(); - } catch (std::exception ex) { + } catch (std::exception & ex) { // failed to generate extended message return m_msg.c_str(); } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 49a7b200a..c6f1b716c 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -213,7 +213,7 @@ format group(format const & f) { format above(format const & f1, format const & f2) { return format{f1, line(), f2}; } -format bracket(std::string const l, format const & x, std::string const r) { +format bracket(std::string const & l, format const & x, std::string const & r) { return group(nest(l.size(), format{format(l), x, format(r)})); } format paren(format const & x) { diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 4aa241ee5..1619516bf 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -192,7 +192,7 @@ public: friend format group(format const & f); friend format above(format const & f1, format const & f2); - friend format bracket(std::string const l, format const & x, std::string const r); + friend format bracket(std::string const & l, format const & x, std::string const & r); friend format wrap(format const & f1, format const & f2); // x + y = x <> y @@ -241,7 +241,7 @@ format const & colon(); format const & dot(); format group(format const & f); format above(format const & f1, format const & f2); -format bracket(std::string const l, format const & x, std::string const r); +format bracket(std::string const & l, format const & x, std::string const & r); format paren(format const & x); format wrap(format const & f1, format const & f2);