Disallow construction of (_ BitVec 0).
authorMorgan Deters <mdeters@cs.nyu.edu>
Fri, 17 May 2013 12:59:25 +0000 (08:59 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Mon, 20 May 2013 20:54:27 +0000 (16:54 -0400)
Thanks to David Cok for reporting this issue.

src/parser/cvc/Cvc.g
src/parser/smt2/Smt2.g

index 217e7ab97aa72837c2c9b4e2b5bb9bfca990e959..778b85fce44e07676c10702092824e524604a1c1 100644 (file)
@@ -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(); }
index 76708807fdb2fa39e7c522c5ca72c6e6c12d8666..6c98a552984cf0b37fbba891d9921fa310c0f614 100644 (file)
@@ -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;