Move promotion rule application to C front-end

The front-ends handle type conversion when doing arithmetic over enum types. The
case of an enum tag is not expected in goto-program conversion. That, however,
was only the case for some operators. Made the C front-end properly handle all
assignment operators.

Author: tautschnig

regression/cbmc/enum8/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+enum E
+{
+  A = 1,
+  B = 16
+};
+
+int main()
+{
+  enum E e = A;
+  e <<= 4;
+  assert(e == B);
+  e >>= 4;
+  assert(e == A);
+  e |= B;
+  e ^= A;
+  assert(e == B);
+  e -= 15;
+  assert(e == A);
+  return 0;
+}

regression/cbmc/enum8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -3344,6 +3344,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
   else if(statement==ID_assign_shl ||
           statement==ID_assign_shr)
   {
+    implicit_typecast_arithmetic(op0);
     implicit_typecast_arithmetic(op1);
 
     if(is_number(op1.type()))
@@ -3358,12 +3359,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
 
         typet underlying_type=op0.type();
 
-        if(underlying_type.id()==ID_c_enum_tag)
-        {
-          const auto &c_enum_type = to_c_enum_tag_type(underlying_type);
-          underlying_type=c_enum_type.subtype();
-        }
-
         if(underlying_type.id()==ID_unsignedbv ||
            underlying_type.id()==ID_c_bool)
         {
@@ -3399,7 +3394,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
             o_type0.id()==ID_signedbv ||
             o_type0.id()==ID_c_bit_field)
     {
-      implicit_typecast(op1, o_type0);
+      implicit_typecast_arithmetic(op0, op1);
       return;
     }
     else if(o_type0.id()==ID_vector &&

src/goto-programs/goto_convert_side_effect.cpp

@@ -105,19 +105,10 @@ void goto_convertt::remove_assignment(
       tmp.op0().make_typecast(expr.op1().type());
       rhs=typecast_exprt(is_not_zero(tmp, ns), expr.op0().type());
     }
-    else if(op0_type.id() == ID_c_enum_tag)
-    {
-      // We convert c_enums to their underlying type, do the
-      // operation, and then convert back
-      const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(op0_type));
-      auto underlying_type = enum_type.subtype();
-      auto op0 = typecast_exprt(expr.op0(), underlying_type);
-      auto op1 = typecast_exprt(expr.op1(), underlying_type);
-      binary_exprt tmp(op0, new_id, op1, underlying_type);
-      rhs = typecast_exprt(tmp, expr.op0().type());
-    }
     else
     {
+      PRECONDITION(
+        op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum);
       rhs.id(new_id);
       rhs.copy_to_operands(expr.op0(), expr.op1());
       rhs.type()=expr.op0().type();