Verilog: grammar for tagged unions

This adds the grammar for tagged union types and tagged union expressions.
The type checker errors these as unsupported.

Author: kroening

regression/verilog/unions/tagged_union1.desc

@@ -0,0 +1,8 @@
+CORE
+tagged_union1.sv
+
+^file .* line 9: no support for tagged unions$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/verilog/unions/tagged_union1.sv

@@ -0,0 +1,11 @@
+module main;
+  typedef union tagged {
+    void Invalid;
+    int Valid;
+  } VInt;
+
+  VInt v;
+
+  initial v = tagged Invalid;
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -140,6 +140,7 @@ IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(verilog_property_declaration)
 IREP_ID_ONE(verilog_sequence_declaration)
 IREP_ID_ONE(verilog_sequence)
+IREP_ID_ONE(verilog_tagged_union)
 IREP_ID_ONE(verilog_value_range)
 IREP_ID_ONE(verilog_void)
 IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)

src/verilog/parser.y

@@ -2161,6 +2161,7 @@ unsized_dimension: '[' ']'
 struct_union:
 	  TOK_STRUCT { init($$, ID_struct); }
 	| TOK_UNION { init($$, ID_union); }
+	| TOK_UNION TOK_TAGGED { init($$, ID_union); }
 	;
 
 // System Verilog standard 1800-2017
@@ -4341,6 +4342,12 @@ expression:
 	| TOK_QSTRING
 		{ init($$, ID_constant); stack_expr($$).type()=typet(ID_string); addswap($$, ID_value, $1); }
 	| inside_expression
+	| tagged_union_expression
+	;
+
+tagged_union_expression:
+	  TOK_TAGGED member_identifier
+		{ init($$, ID_verilog_tagged_union); mto($$, $2); }
 	;
 
 inside_expression:

src/verilog/verilog_typecheck_expr.cpp

@@ -2819,6 +2819,11 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     // assignment patterns, 1800 2017 10.9
     convert_expr(expr.op());
   }
+  else if(expr.id() == ID_verilog_tagged_union)
+  {
+    throw errort{}.with_location(expr.source_location())
+      << "no support for tagged unions";
+  }
   else
   {
     throw errort() << "no conversion for unary expression " << expr.id();