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/compat/cvc3_compat.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/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 0ecc6b5c7..601c251d9 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -2273,7 +2273,7 @@ void ValidityChecker::popto(int stackLevel) { } int ValidityChecker::scopeLevel() { - return d_parserContext->getDeclarationLevel(); + return d_parserContext->scopeLevel(); } void ValidityChecker::pushScope() { @@ -2287,12 +2287,12 @@ void ValidityChecker::popScope() { void ValidityChecker::poptoScope(int scopeLevel) { CVC4::CheckArgument(scopeLevel >= 0, scopeLevel, "Cannot pop to a negative scope level %d", scopeLevel); - CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), + CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(), scopeLevel, "Cannot pop to a scope level higher than the current one! " "At scope level %u, user requested scope level %d", - d_parserContext->getDeclarationLevel(), scopeLevel); - while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) { + d_parserContext->scopeLevel(), scopeLevel); + while(unsigned(scopeLevel) < d_parserContext->scopeLevel()) { popScope(); } } |