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
This commit is contained in:
Leonardo de Moura 2017-05-31 18:05:03 -07:00
parent ac17270894
commit 24048c4258
6 changed files with 35 additions and 16 deletions

View file

@ -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<module_name> imports;
for (name const & n : to_list_name_ref(modules)) {
imports.push_back({n, optional<unsigned>()});
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));

View file

@ -2337,31 +2337,35 @@ void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & im
prelude = true;
}
if (!prelude) {
imports.push_back({ "init", optional<unsigned>() });
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<unsigned> 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<module_name> & 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;

View file

@ -700,8 +700,8 @@ public:
scoped_expr_caching disable(false);
auto mod_ldr = mk_olean_loader(m_path);
optional<unsigned> 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 {

View file

@ -25,6 +25,9 @@ public:
struct module_name {
name m_name;
optional<unsigned> 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;

View file

@ -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 <list>
#include <string>
#include <vector>
@ -26,7 +32,6 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
#include "shell/server.h"
namespace lean {
struct all_messages_msg {
std::vector<message> m_msgs;

View file

@ -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<T>(other.m_value));
}
explicit optional(T const & v):m_some(true) {