Merge pull request #1374 from diffblue/smv-enum-vs-var

SMV: move logic that distinguishes enums and vars to type checker

Author: tautschnig

src/smvlang/parser.y

@@ -952,32 +952,8 @@ identifier : IDENTIFIER_Token
 variable_identifier: complex_identifier
            {
              auto id = merge_complex_identifier(stack_expr($1));
-
-             bool is_enum=(PARSER.module->enum_set.find(id)!=
-                           PARSER.module->enum_set.end());
-             bool is_var=(PARSER.module->vars.find(id)!=
-                          PARSER.module->vars.end());
-
-             if(is_var && is_enum)
-             {
-               yyerror("identifier `"+id2string(id)+"' is ambiguous");
-               YYERROR;
-             }
-             else if(is_enum)
-             {
-               init($$, ID_constant);
-               stack_expr($$).type()=typet(ID_smv_enumeration);
-               stack_expr($$).set(ID_value, id);
-             }
-             else // not an enum, probably a variable
-             {
-               init($$, ID_smv_identifier);
-               stack_expr($$).set(ID_identifier, id);
-               auto var_it = PARSER.module->vars.find(id);
-               if(var_it!= PARSER.module->vars.end())
-                 stack_expr($$).type()=var_it->second.type;
-               //PARSER.module->vars[stack_expr($1).id()];
-             }
+             init($$, ID_smv_identifier);
+             stack_expr($$).set(ID_identifier, id);
            }
            | STRING_Token
            {

src/smvlang/smv_typecheck.cpp

@@ -1708,10 +1708,21 @@ void smv_typecheckt::convert(exprt &expr)
     DATA_INVARIANT(
       identifier.find("::") == std::string::npos, "conversion is done once");
 
-    std::string id = module + "::var::" + identifier;
+    // enum or variable?
+    if(modulep->enum_set.find(identifier) == modulep->enum_set.end())
+    {
+      std::string id = module + "::var::" + identifier;
 
-    expr.set(ID_identifier, id);
-    expr.id(ID_symbol);
+      expr.set(ID_identifier, id);
+      expr.id(ID_symbol);
+    }
+    else
+    {
+      expr.id(ID_constant);
+      expr.type() = typet(ID_smv_enumeration);
+      expr.set(ID_value, identifier);
+      expr.remove(ID_identifier);
+    }
   }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")