diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 18:14:18 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-20 17:00:56 -0400 |
commit | 0e6d0a7bced1083db25a286b5ddfd79fba344639 (patch) | |
tree | a5d75edb81df8f6ce0c904b5cb20870faa6d3bc0 /src/parser/parser.cpp | |
parent | aef543d74c4fb23a86ad2986d67e7fc7f11d1feb (diff) |
Detect multiply-defined :named annotations and issue an error.
Thanks to David Cok for pointing out this issue.
Conflicts:
library_versions
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 198d1cc31..1c275add7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -357,7 +357,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: - return d_symtab->isBound(name); + return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name); case SYM_SORT: return d_symtab->isBoundType(name); } @@ -365,6 +365,11 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { return false; } +void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) { + checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE); + d_reservedSymbols.insert(varName); +} + void Parser::checkDeclaration(const std::string& varName, DeclarationCheck check, SymbolType type) |