diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 08:59:25 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 08:59:25 -0400 |
| commit | 067f3f556a84c1af54d4ef2188d1b145d02b26e3 (patch) | |
| tree | 3839c3a84f865dcd84d1104a04acf3a10b8433cf /src/parser | |
| parent | 5ad796d0ddaa9c6f2ad98d2680babb7776a5f9b0 (diff) | |
Disallow construction of (_ BitVec 0).
Thanks to David Cok for reporting this issue.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 6 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 217e7ab97..778b85fce 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1184,7 +1184,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, /* bitvector types */ | BITVECTOR_TOK LPAREN k=numeral RPAREN - { t = EXPR_MANAGER->mkBitVectorType(k); } + { if(k == 0) { + PARSER_STATE->parseError("Illegal bitvector size: 0"); + } + t = EXPR_MANAGER->mkBitVectorType(k); + } /* basic types */ | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 76708807f..6c98a5529 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1204,6 +1204,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] if( numerals.size() != 1 ) { PARSER_STATE->parseError("Illegal bitvector type."); } + if(numerals.front() == 0) { + PARSER_STATE->parseError("Illegal bitvector size: 0"); + } t = EXPR_MANAGER->mkBitVectorType(numerals.front()); } else { std::stringstream ss; |