SMV: add source locations to identifiers

This adds a constructor to smv_identifier_exprt with source location, and
uses this constructor in the parser.

Author: kroening

src/smvlang/parser.y

@@ -411,17 +411,13 @@ ivar_declaration:
 ivar_simple_var_list:
              identifier ':' simple_type_specifier ';'
            {
-             irep_idt identifier = stack_expr($1).id();
-             stack_expr($1).id(ID_smv_identifier);
-             stack_expr($1).set(ID_identifier, identifier);
-             PARSER.module->add_ivar(stack_expr($1), stack_type($3));
+             smv_identifier_exprt identifier{stack_expr($1).id(), PARSER.source_location()};
+             PARSER.module->add_ivar(std::move(identifier), stack_type($3));
            }
            | ivar_simple_var_list identifier ':' simple_type_specifier ';'
            {
-             irep_idt identifier = stack_expr($2).id();
-             stack_expr($2).id(ID_smv_identifier);
-             stack_expr($2).set(ID_identifier, identifier);
-             PARSER.module->add_ivar(stack_expr($2), stack_type($4));
+             smv_identifier_exprt identifier{stack_expr($2).id(), PARSER.source_location()};
+             PARSER.module->add_ivar(std::move(identifier), stack_type($4));
            }
            ;
 
@@ -686,11 +682,8 @@ enum_element: IDENTIFIER_Token
            {
              $$=$1;
              PARSER.module->enum_set.insert(stack_expr($1).id_string());
-
-             exprt expr(ID_smv_identifier);
-             expr.set(ID_identifier, stack_expr($1).id());
-             PARSER.set_source_location(expr);
-             PARSER.module->add_enum(std::move(expr));
+             PARSER.module->add_enum(
+               smv_identifier_exprt{stack_expr($1).id(), PARSER.source_location()});
            }
            ;
 
@@ -795,9 +788,7 @@ basic_expr : constant
              // This rule is part of "complex_identifier" in the NuSMV manual.
              $$ = $1;
              irep_idt identifier = stack_expr($$).id();
-             stack_expr($$).id(ID_smv_identifier);
-             stack_expr($$).set(ID_identifier, identifier);
-             PARSER.set_source_location(stack_expr($$));
+             stack_expr($$) = smv_identifier_exprt{identifier, PARSER.source_location()};
            }
            | basic_expr DOT_Token IDENTIFIER_Token
            {
@@ -961,9 +952,8 @@ complex_identifier:
              identifier
            {
              $$ = $1;
-             irep_idt identifier = stack_expr($$).id();
-             stack_expr($$).id(ID_smv_identifier);
-             stack_expr($$).set(ID_identifier, identifier);
+             auto identifier = stack_expr($$).id();
+             stack_expr($$) = smv_identifier_exprt{identifier, PARSER.source_location()};
            }
            | complex_identifier DOT_Token QIDENTIFIER_Token
            {

src/smvlang/smv_expr.h

@@ -337,6 +337,15 @@ class smv_identifier_exprt : public nullary_exprt
     identifier(_identifier);
   }
 
+  explicit smv_identifier_exprt(
+    irep_idt _identifier,
+    source_locationt _location)
+    : smv_identifier_exprt{_identifier}
+  {
+    if(_location.is_not_nil())
+      add_source_location() = _location;
+  }
+
   irep_idt identifier() const
   {
     return get(ID_identifier);