SMV: word constants

This adds NuSMV's word constants to scanner, parser, type checker.

Author: kroening

regression/smv/word/word_constants1.desc

@@ -0,0 +1,7 @@
+CORE
+word_constants1.smv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/word/word_constants1.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+SPEC uwconst(123, 8) = 0d8_123;
+SPEC uwconst(123, 8) = 0ud8_123;
+SPEC uwconst(123, 8) = 0h_7b;
+SPEC uwconst(123, 8) = 0uh_7b;
+SPEC uwconst(123, 8) = 0b_01111011;
+SPEC uwconst(123, 8) = 0ub_01111011;
+SPEC uwconst(123, 8) = 0b8_1111011;
+SPEC uwconst(123, 8) = 0ub8_1111011;
+
+SPEC swconst(123, 8) = 0sd8_123;
+SPEC swconst(123, 8) = 0sh_7b;
+SPEC swconst(123, 8) = 0sb_01111011;
+SPEC swconst(123, 8) = 0sb8_1111011;

src/smvlang/parser.y

@@ -6,6 +6,7 @@
 #include "smv_parser.h"
 #include "smv_typecheck.h"
 
+#include <util/bitvector_types.h>
 #include <util/mathematical_types.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
@@ -320,8 +321,9 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
 
 %token IDENTIFIER_Token   "identifier"
 %token QIDENTIFIER_Token  "quoted identifier"
-%token STRING_Token    "quoted string"
+%token STRING_Token   "quoted string"
 %token NUMBER_Token   "number"
+%token WORD_CONSTANT_Token "word constant"
 
 /* operator precedence, low to high */
 %right IMPLIES_Token
@@ -815,6 +817,7 @@ formula    : basic_expr
 
 constant   : boolean_constant
            | integer_constant
+           | word_constant
            ;
 
 boolean_constant:
@@ -841,6 +844,15 @@ integer_constant:
            }
            ;
 
+word_constant:
+             WORD_CONSTANT_Token
+           {
+             init($$, ID_constant);
+             stack_expr($$).set(ID_value, stack_expr($1).id());
+             stack_expr($$).type() = bv_typet{0};
+           }
+           ;
+
 basic_expr : constant
            | identifier
            {

src/smvlang/scanner.l

@@ -188,6 +188,11 @@ void newlocation(YYSTYPE &x)
                   stack_expr(yysmvlval).id(yytext);
 		  return NUMBER_Token;
 		}
+0[us]?[bBoOdDhH][0-9]*_[0-9a-fA-F][_0-9a-fA-F]* {
+                  newstack(yysmvlval);
+                  stack_expr(yysmvlval).id(yytext);
+		  return WORD_CONSTANT_Token;
+		}
 \"[^\"]*\"      {
                   newstack(yysmvlval);
                   std::string tmp(yytext);