Merge pull request #373 from diffblue/verilog-enum-decay

Verilog: enums decay when used in relational/arithmetic operators

Author: tautschnig

regression/verilog/data-types/enum_initializers1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 enum_initializers1.sv
-
-^EXIT=10$
+--bound 0
+^\[main\.property\.pA\] always 1 == 1: PROVED up to bound 0$
+^\[main\.property\.pB\] always 1 \+ 10 == 11: PROVED up to bound 0$
+^EXIT=0$
 ^SIGNAL=0$
 --
 --
-Crashes with missing identifier
-

src/verilog/verilog_typecheck_expr.cpp

@@ -1665,8 +1665,23 @@ void verilog_typecheck_exprt::tc_binary_expr(
   const exprt &expr,
   exprt &op0, exprt &op1)
 {
-  const typet new_type=max_type(op0.type(), op1.type());
-  
+  // Verilog enum types decay to their base type when used in relational
+  // or arithmetic expressions.
+  auto enum_decay = [](const typet &type) {
+    if(type.get(ID_C_verilog_type) == ID_verilog_enum)
+    {
+      typet result = type;
+      result.remove(ID_C_verilog_type);
+      result.remove(ID_C_identifier);
+      return result;
+    }
+    else
+      return type;
+  };
+
+  const typet new_type =
+    max_type(enum_decay(op0.type()), enum_decay(op1.type()));
+
   if(new_type.is_nil())
   {
     throw errort().with_location(expr.source_location())