Merge pull request #846 from diffblue/verilog_lowering_type

Verilog: lowering for types

src/verilog/verilog_lowering.cpp

@@ -416,3 +416,11 @@ exprt verilog_lowering(exprt expr)
 
   UNREACHABLE;
 }
+
+typet verilog_lowering(typet type)
+{
+  if(type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
+    return lower_to_aval_bval(type);
+  else
+    return type;
+}

src/verilog/verilog_lowering.h

@@ -10,7 +10,9 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_VERILOG_LOWERING_H
 
 class exprt;
+class typet;
 
 exprt verilog_lowering(exprt);
+typet verilog_lowering(typet);
 
 #endif

src/verilog/verilog_synthesis.cpp

@@ -3314,6 +3314,10 @@ exprt verilog_synthesist::symbol_expr(
 {
   exprt result=exprt(curr_or_next==NEXT?ID_next_symbol:ID_symbol, symbol.type);
   result.set(ID_identifier, symbol.name);
+
+  // The type may need to be lowered
+  result.type() = verilog_lowering(result.type());
+
   return result;
 }