michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean): memory access violation

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-14 15:37:45 -07:00
parent 45684588cc
commit 01f8f3c11d
3 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser_config.cpp
View file

@ -415,14 +415,16 @@ environment override_notation(environment const & env, name const & n, bool pers
environment r = env;
bool found = false;
if (auto it = token_ext::get_entries(r, n)) {
list<token_entry> entries = *it;
found = true;
for (token_entry e : *it) {
for (token_entry e : entries) {
r = add_token(r, e, persistent);
}
}
if (auto it = notation_ext::get_entries(env, n)) {
list<notation_entry> entries = *it;
found = true;
for (notation_entry const & e : *it) {
for (notation_entry const & e : entries) {
notation_entry new_e(e, false);
r = add_notation(r, new_e, persistent);
}

8
src/frontends/lean/scanner.cpp
View file

@ -403,8 +403,8 @@ auto scanner::read_key_cmd_id() -> token_kind {
return token_kind::Identifier;
} else {
move_back(cs.size() - key_sz, num_utfs - key_utf_sz);
m_token_info = info;
return info->is_command() ? token_kind::CommandKeyword : token_kind::Keyword;
m_token_info = *info;
return m_token_info.is_command() ? token_kind::CommandKeyword : token_kind::Keyword;
}
}
@ -447,7 +447,7 @@ auto scanner::scan(environment const & env) -> token_kind {
token_kind k = read_key_cmd_id();
if (k == token_kind::Keyword) {
// We treat '(--', '(*', '--' as "keywords.
name const & n = m_token_info->value();
name const & n = m_token_info.value();
if (n == *g_begin_comment_tk)
read_single_line_comment();
else if (n == *g_begin_comment_block_tk)
@ -465,7 +465,7 @@ auto scanner::scan(environment const & env) -> token_kind {
}
scanner::scanner(std::istream & strm, char const * strm_name, unsigned line):
m_tokens(nullptr), m_stream(strm), m_token_info(nullptr) {
m_tokens(nullptr), m_stream(strm) {
m_stream_name = strm_name ? strm_name : "[unknown]";
m_sline = line;
m_line = line;

4
src/frontends/lean/scanner.h
View file

@ -40,7 +40,7 @@ protected:
int m_line; // line of the token
name m_name_val;
token_info const * m_token_info;
token_info m_token_info;
mpq m_num_val;
std::string m_buffer;
std::string m_aux_buffer;
@ -77,7 +77,7 @@ public:
mpq const & get_num_val() const { return m_num_val; }
name const & get_name_val() const { return m_name_val; }
std::string const & get_str_val() const { return m_buffer; }
token_info const & get_token_info() const { lean_assert(m_token_info); return *m_token_info; }
token_info const & get_token_info() const { return m_token_info; }
std::string const & get_stream_name() const { return m_stream_name; }
};