Merge pull request #1479 from diffblue/show-modules-smv

Implement `--show-modules` for SMV

Author: tautschnig

regression/ebmc/CLI/show-modules-smv.desc

@@ -0,0 +1,21 @@
+CORE
+show-modules-smv.smv
+--show-modules
+activate-multi-line-match
+Module 1:
+  Location:   file show-modules-smv\.smv line 3
+  Identifier: smv::main
+  Name:       main
+
+Module 2:
+  Location:   file show-modules-smv\.smv line 8
+  Identifier: smv::bar
+  Name:       bar
+
+Module 3:
+  Location:   file show-modules-smv\.smv line 13
+  Identifier: smv::foo
+  Name:       foo
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/CLI/show-modules-smv.smv

@@ -0,0 +1,15 @@
+-- from the NuSMV 2.7 manual
+
+MODULE main
+ VAR
+  a : bar;
+  m : foo(a);
+
+MODULE bar
+ VAR
+  q : boolean;
+  p : boolean;
+
+MODULE foo(c)
+ DEFINE
+  flag := c.q | c.p;

src/smvlang/parser.y

@@ -177,7 +177,7 @@ Function: new_module
 
 \*******************************************************************/
 
-static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
+static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_name)
 {
   auto base_name = stack_expr(module_name).id_string();
   const std::string identifier=smv_module_symbol(base_name);
@@ -186,6 +186,7 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
   PARSER.parse_tree.module_map[identifier] = --PARSER.parse_tree.module_list.end();
   module.name = identifier;
   module.base_name = base_name;
+  module.source_location = stack_expr(location).source_location();
   PARSER.module = &module;
   return module;
 }
@@ -363,8 +364,11 @@ module_name: IDENTIFIER_Token
            | STRING_Token
            ;
 
-module_head: MODULE_Token module_name { new_module($2); }
-           | MODULE_Token module_name { new_module($2); }
+module_keyword: MODULE_Token { init($$); /* for the location */ }
+           ;
+
+module_head: module_keyword module_name { new_module($1, $2); }
+           | module_keyword module_name { new_module($1, $2); }
              '(' module_parameters_opt ')'
            ;
 

src/smvlang/smv_ebmc_language.cpp

@@ -70,9 +70,26 @@ std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
     return {};
   }
 
-  if(
-    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-    cmdline.isset("json-modules"))
+  if(cmdline.isset("show-modules"))
+  {
+    std::size_t count = 0;
+    auto &out = std::cout;
+
+    for(const auto &module : parse_tree.module_list)
+    {
+      count++;
+
+      out << "Module " << count << ":" << '\n';
+
+      out << "  Location:   " << module.source_location << '\n';
+      out << "  Identifier: " << module.name << '\n';
+      out << "  Name:       " << module.base_name << '\n' << '\n';
+    }
+
+    return {};
+  }
+
+  if(cmdline.isset("modules-xml") || cmdline.isset("json-modules"))
   {
     //show_modules(cmdline, message_handler);
     return {};

src/smvlang/smv_parse_tree.h

@@ -29,6 +29,7 @@ class smv_parse_treet
 
   struct modulet
   {
+    source_locationt source_location;
     irep_idt name, base_name;
     std::vector<irep_idt> parameters;