Merge pull request #1124 from diffblue/smv-identifier-tokens

SMV: rename `STRING_Token`, `QSTRING_Token` and `QUOTE_Token`

Author: tautschnig

regression/smv/syntax-errors/syntax1.desc

@@ -1,7 +1,7 @@
 CORE
 syntax1.smv
 
-^file .* line 3: syntax error, unexpected VAR, expecting string or "'" before 'VAR'$
+^file .* line 3: syntax error, unexpected VAR, expecting identifier or quoted string before 'VAR'$
 ^EXIT=1$
 ^SIGNAL=0$
 --

regression/smv/syntax-errors/syntax3.desc

@@ -1,7 +1,7 @@
 CORE
 syntax3.smv
 
-^file .* line 3: syntax error, unexpected string, expecting number before 'not_a_number'$
+^file .* line 3: syntax error, unexpected identifier, expecting number before 'not_a_number'$
 ^EXIT=1$
 ^SIGNAL=0$
 --

src/smvlang/parser.y

@@ -273,9 +273,9 @@ static void new_module(YYSTYPE &module)
 %token ADD_Token
 %token SUB_Token
 
-%token STRING_Token   "string"
-%token QSTRING_Token  "quoted string"
-%token QUOTE_Token    "'"
+%token IDENTIFIER_Token   "identifier"
+%token QIDENTIFIER_Token  "quoted identifier"
+%token STRING_Token    "quoted string"
 %token NUMBER_Token   "number"
 
 /* operator precedence, low to high */
@@ -310,8 +310,8 @@ modules    : module
 module     : module_head module_body
            ;
 
-module_name: STRING_Token
-           | QUOTE_Token
+module_name: IDENTIFIER_Token
+           | STRING_Token
            ;
 
 module_head: MODULE_Token module_name { new_module($2); }
@@ -421,7 +421,7 @@ ltl_specification:
            }
            ;
 
-extern_var : variable_identifier EQUAL_Token QUOTE_Token
+extern_var : variable_identifier EQUAL_Token STRING_Token
            {
              const irep_idt &identifier=stack_expr($1).get(ID_identifier);
              smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
@@ -532,7 +532,7 @@ enum_list  : enum_element
            }
            ;
 
-enum_element: STRING_Token
+enum_element: IDENTIFIER_Token
            {
              $$=$1;
              PARSER.module->enum_set.insert(stack_expr($1).id_string());
@@ -783,7 +783,12 @@ formula_list:
            | formula_list ',' formula { $$=$1; mto($$, $3); }
            ;
 
-identifier : STRING_Token
+identifier : IDENTIFIER_Token
+           | QIDENTIFIER_Token
+           {
+             // not supported by NuSMV
+             init($$, std::string(stack_expr($1).id_string(), 1)); // remove backslash
+           }
            ;
 
 variable_identifier: complex_identifier
@@ -816,7 +821,7 @@ variable_identifier: complex_identifier
                //PARSER.module->vars[stack_expr($1).id()];
              }
            }
-           | QUOTE_Token
+           | STRING_Token
            {
              const irep_idt &id=stack_expr($1).id();
 
@@ -826,19 +831,16 @@ variable_identifier: complex_identifier
            }
            ;
 
-complex_identifier: QSTRING_Token
-           {
-             init($$, std::string(stack_expr($1).id_string(), 1)); // remove backslash
-           }
-           | STRING_Token
-           | complex_identifier DOT_Token QSTRING_Token
+complex_identifier:
+             identifier
+           | complex_identifier DOT_Token QIDENTIFIER_Token
            {
              std::string id(stack_expr($1).id_string());
              id+=".";
              id+=std::string(stack_expr($3).id_string(), 1); // remove backslash
              init($$, id);
            }
-           | complex_identifier DOT_Token STRING_Token
+           | complex_identifier DOT_Token IDENTIFIER_Token
            {
              std::string id(stack_expr($1).id_string());
              id+=".";

src/smvlang/scanner.l

@@ -176,12 +176,12 @@ void newlocation(YYSTYPE &x)
 [\$A-Za-z_][A-Za-z0-9_\$#-]*	{
                   newstack(yysmvlval);
                   stack_expr(yysmvlval).id(yytext);
-		  return STRING_Token;
+		  return IDENTIFIER_Token;
 		}
 \\[A-Za-z0-9_\$#-]*	{
                   newstack(yysmvlval);
                   stack_expr(yysmvlval).id(yytext);
-		  return QSTRING_Token;
+		  return QIDENTIFIER_Token;
 		}
 [0-9][0-9]*	{
                   newstack(yysmvlval);
@@ -192,7 +192,7 @@ void newlocation(YYSTYPE &x)
                   newstack(yysmvlval);
                   std::string tmp(yytext);
                   stack_expr(yysmvlval).id(std::string(tmp, 1, tmp.size()-2));
-                  return QUOTE_Token;
+                  return STRING_Token;
                 }
 
 "?"		return IF_Token;