Merge pull request #1492 from diffblue/expr2verilog-struct

Verilog: format struct expressions

Author: tautschnig

regression/verilog/expressions/static_cast4.desc

@@ -1,6 +1,7 @@
 CORE
 static_cast4.sv
 --module main
+^\[.*\] struct packed'\('\{ a: 1, b: 2 \}\) == main\.some_struct: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/verilog/expr2verilog.cpp

@@ -1540,6 +1540,43 @@ expr2verilogt::resultt expr2verilogt::convert_sequence_property_instance(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_struct
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_struct(const struct_exprt &src)
+{
+  std::string dest = "'{";
+
+  auto &type = to_struct_type(src.type());
+  DATA_INVARIANT(
+    type.components().size() == src.operands().size(),
+    "number of compontents must match");
+
+  for(std::size_t index = 0; index < src.operands().size(); index++)
+  {
+    auto &op = src.operands()[index];
+    if(index != 0)
+      dest += ',';
+    dest += ' ';
+    dest += id2string(type.components()[index].get_name());
+    dest += ": ";
+    dest += convert_rec(op).s;
+  }
+
+  dest += " }";
+
+  return {verilog_precedencet::MAX, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_value_range
 
   Inputs:
@@ -2081,6 +2118,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
       to_sva_sequence_property_instance_expr(src));
   }
 
+  else if(src.id() == ID_struct)
+  {
+    return convert_struct(to_struct_expr(src));
+  }
+
   // no VERILOG language expression for internal representation
   return convert_norep(src);
 }

src/verilog/expr2verilog_class.h

@@ -187,6 +187,8 @@ class expr2verilogt
   resultt convert_sequence_property_instance(
     const class sva_sequence_property_instance_exprt &);
 
+  resultt convert_struct(const struct_exprt &);
+
 protected:
   const namespacet &ns;
 };