SMV: store module parameter list in parse tree

regression/smv/modules/parameters1.desc

@@ -0,0 +1,12 @@
+CORE
+parameters1.smv
+--show-parse
+^  PARAMETERS:$
+^    pa$
+^    pb$
+^    pc$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/modules/parameters1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+MODULE my-module(pa, pb, pc)

src/smvlang/parser.y

@@ -175,12 +175,15 @@ Function: new_module
 
 \*******************************************************************/
 
-static void new_module(YYSTYPE &module)
+static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
 {
-  const std::string name=smv_module_symbol(stack_expr(module).id_string());
-  PARSER.module=&PARSER.parse_tree.modules[name];
-  PARSER.module->name=name;
-  PARSER.module->base_name=stack_expr(module).id_string();
+  auto base_name = stack_expr(module_name).id_string();
+  const std::string identifier=smv_module_symbol(base_name);
+  auto &module=PARSER.parse_tree.modules[identifier];
+  module.name = identifier;
+  module.base_name = base_name;
+  PARSER.module = &module;
+  return module;
 }
 
 /*------------------------------------------------------------------------*/
@@ -356,7 +359,11 @@ module_name: IDENTIFIER_Token
            ;
 
 module_head: MODULE_Token module_name { new_module($2); }
-           | MODULE_Token module_name { new_module($2); } '(' module_parameters_opt ')'
+           | MODULE_Token module_name '(' module_parameters_opt ')'
+           {
+             auto &module = new_module($2);
+             module.parameters = stack_expr($4);
+           }
            ;
 
 module_body: /* optional */
@@ -566,10 +573,22 @@ module_parameter: identifier
 
 module_parameters:
              module_parameter
+           {
+             init($$);
+             mto($$, $1);
+           }
            | module_parameters ',' module_parameter
+           {
+             $$ = $1;
+             mto($$, $3);
+           }
            ;
 
-module_parameters_opt: /* empty */
+module_parameters_opt:
+             /* empty */
+           {
+             init($$);
+           }
            | module_parameters
            ;
 

src/smvlang/smv_language.cpp

@@ -134,6 +134,13 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
     const smv_parse_treet::modulet &module=it->second;
     out << "Module: " << module.name << std::endl << std::endl;
 
+    out << "  PARAMETERS:\n";
+
+    for(auto &parameter : module.parameters.get_sub())
+      out << "    " << parameter.id() << '\n';
+
+    out << '\n';
+
     out << "  VARIABLES:" << std::endl;
 
     for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin();

src/smvlang/smv_parse_tree.h

@@ -37,7 +37,8 @@ class smv_parse_treet
   struct modulet
   {
     irep_idt name, base_name;
-
+    irept parameters;
+
     struct itemt
     {
       enum item_typet