From 24048c42584f12c476377ddda752fe5178271b87 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 May 2017 18:05:03 -0700 Subject: [PATCH] fix(*): gcc 7 weird uninitialized warnings I think most of them are incorrect. I didn't find a workaround for the one at json.hpp. So, I just disabled this warning at server.cpp --- src/api/module.cpp | 3 ++- src/frontends/lean/parser.cpp | 32 +++++++++++++++++++++----------- src/frontends/smt2/parser.cpp | 4 ++-- src/library/module.h | 3 +++ src/shell/server.cpp | 7 ++++++- src/util/optional.h | 2 +- 6 files changed, 35 insertions(+), 16 deletions(-) diff --git a/src/api/module.cpp b/src/api/module.cpp index d6d377ba39..e181fa7c42 100644 --- a/src/api/module.cpp +++ b/src/api/module.cpp @@ -24,7 +24,8 @@ lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, le auto new_env = to_env_ref(env); std::vector imports; for (name const & n : to_list_name_ref(modules)) { - imports.push_back({n, optional()}); + module_name m(n); + imports.push_back(m); } new_env = import_modules(new_env, "", imports, mk_olean_loader(standard_search_path().get_path())); *r = of_env(new environment(new_env)); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3515dcab69..7467ea9c44 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2337,31 +2337,35 @@ void parser::parse_imports(unsigned & fingerprint, std::vector & im prelude = true; } if (!prelude) { - imports.push_back({ "init", optional() }); + module_name m("init"); + imports.push_back(m); } while (curr_is_token(get_import_tk())) { m_last_cmd_pos = pos(); next(); while (true) { - pos_info p = pos(); - optional k; + pos_info p = pos(); + bool k_init = false; + unsigned k = 0; try { unsigned h = 0; while (true) { if (curr_is_token(get_period_tk())) { - if (!k) { + if (!k_init) { k = 0; + k_init = true; } else { - k = *k + 1; + k = k + 1; h++; } next(); } else if (curr_is_token(get_ellipsis_tk())) { - if (!k) { + if (!k_init) { k = 2; + k_init = true; h = 2; } else { - k = *k + 3; + k = k + 3; h += 3; } next(); @@ -2374,14 +2378,20 @@ void parser::parse_imports(unsigned & fingerprint, std::vector & im break; name f = get_name_val(); fingerprint = hash(fingerprint, f.hash()); - if (k) { + if (k_init) { fingerprint = hash(fingerprint, h); } - imports.push_back({f, k}); + if (k_init) { + module_name m(f, k); + imports.push_back(m); + } else { + module_name m(f); + imports.push_back(m); + } next(); } catch (break_at_pos_exception & e) { - if (k) - e.m_token_info.m_token = std::string(*k + 1, '.') + e.m_token_info.m_token.to_string(); + if (k_init) + e.m_token_info.m_token = std::string(k + 1, '.') + e.m_token_info.m_token.to_string(); e.m_token_info.m_context = break_at_pos_exception::token_context::import; e.m_token_info.m_pos = p; throw; diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp index 2cbf85f6df..20080ae377 100644 --- a/src/frontends/smt2/parser.cpp +++ b/src/frontends/smt2/parser.cpp @@ -700,8 +700,8 @@ public: scoped_expr_caching disable(false); auto mod_ldr = mk_olean_loader(m_path); - optional k; - m_env = import_modules(m_env, get_stream_name(), {{"init", k}, {"smt", k}}, mod_ldr); + m_env = import_modules(m_env, get_stream_name(), {module_name("init"), module_name("smt")}, + mod_ldr); bool ok = true; try { diff --git a/src/library/module.h b/src/library/module.h index 94421da25f..06f012610c 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -25,6 +25,9 @@ public: struct module_name { name m_name; optional m_relative; + module_name() {} + module_name(name const & n, unsigned k):m_name(n), m_relative(k) {} + explicit module_name(name const & n):m_name(n) {} }; struct modification; diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 774e44c5f1..590451703a 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -5,6 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich */ #if defined(LEAN_JSON) +// Remark: gcc 7 produces a warning at json.hpp +// We believe it is a spurious warning +#if defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wuninitialized" +#endif + #include #include #include @@ -26,7 +32,6 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich #include "shell/server.h" namespace lean { - struct all_messages_msg { std::vector m_msgs; diff --git a/src/util/optional.h b/src/util/optional.h index 56206a2af4..3bd73b640a 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -29,7 +29,7 @@ public: new (&m_value) T(other.m_value); } optional(optional && other):m_some(other.m_some) { - if (m_some) + if (other.m_some) new (&m_value) T(std::forward(other.m_value)); } explicit optional(T const & v):m_some(true) {