Merge pull request #415 from diffblue/empty_item

Verilog: empty module/generate item

Author: tautschnig

regression/verilog/modules/empty_item.desc

@@ -0,0 +1,7 @@
+CORE
+empty_item.v
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/modules/empty_item.v

@@ -0,0 +1,10 @@
+module main;
+  // The empty item.
+  ;
+
+  generate
+    // Also inside generate
+    ;
+  endgenerate
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -137,6 +137,7 @@ IREP_ID_ONE(offset)
 IREP_ID_ONE(xnor)
 IREP_ID_ONE(specify)
 IREP_ID_ONE(verilog_module)
+IREP_ID_ONE(verilog_empty_item)
 IREP_ID_ONE(module_source)
 IREP_ID_ONE(module_items)
 IREP_ID_ONE(parameter_port_list)

src/verilog/parser.y

@@ -1063,6 +1063,8 @@ package_or_generate_item_declaration:
 	     that let constructs may be declared in a
 	     module/interface/program/checker etc. */
 	| let_declaration
+	| ';'
+		{ init($$, ID_verilog_empty_item); }
         ;
 
 // System Verilog standard 1800-2017

src/verilog/verilog_elaborate.cpp

@@ -771,6 +771,9 @@ void verilog_typecheckt::collect_symbols(
   {
     collect_symbols(to_verilog_let(module_item));
   }
+  else if(module_item.id() == ID_verilog_empty_item)
+  {
+  }
   else
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());
 }

src/verilog/verilog_interfaces.cpp

@@ -277,6 +277,9 @@ void verilog_typecheckt::interface_module_item(
   {
     // already done during constant elaboration
   }
+  else if(module_item.id() == ID_verilog_empty_item)
+  {
+  }
   else
   {
     DATA_INVARIANT(false, "unexpected module item: " + module_item.id_string());

src/verilog/verilog_synthesis.cpp

@@ -2633,6 +2633,9 @@ void verilog_synthesist::synth_module_item(
   {
     // done already
   }
+  else if(module_item.id() == ID_verilog_empty_item)
+  {
+  }
   else
   {
     throw errort().with_location(module_item.source_location())

src/verilog/verilog_typecheck.cpp

@@ -1638,6 +1638,9 @@ void verilog_typecheckt::convert_module_item(
   {
     // done already
   }
+  else if(module_item.id() == ID_verilog_empty_item)
+  {
+  }
   else
   {
     throw errort().with_location(module_item.source_location())