From ab6e2d109664f09fd4b9131c66892adc60fa19c5 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 8 Jan 2019 12:09:27 +0000
Subject: [PATCH] fix promotion for C bit fields

promotion rules apply to bit-fields, based on number of bits, not based on
underlying type
---
 regression/cbmc/Bitfields1/test.desc |  2 +-
 src/ansi-c/c_typecast.cpp            | 25 ++++++++++++++++++++++++-
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc/Bitfields1/test.desc b/regression/cbmc/Bitfields1/test.desc
index 52168c7eba4..9efefbc7362 100644
--- a/regression/cbmc/Bitfields1/test.desc
+++ b/regression/cbmc/Bitfields1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index eb31923d73a..b617bf845bc 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -354,7 +354,30 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   else if(type.id()==ID_complex)
     return COMPLEX;
   else if(type.id()==ID_c_bit_field)
-    return get_c_type(to_c_bit_field_type(type).subtype());
+  {
+    const auto &bit_field_type = to_c_bit_field_type(type);
+
+    // We take the underlying type, and then apply the number
+    // of bits given
+    typet underlying_type;
+
+    if(bit_field_type.subtype().id() == ID_c_enum_tag)
+    {
+      const auto &followed =
+        ns.follow_tag(to_c_enum_tag_type(bit_field_type.subtype()));
+      if(followed.is_incomplete())
+        return INT;
+      else
+        underlying_type = followed.subtype();
+    }
+    else
+      underlying_type = bit_field_type.subtype();
+
+    const bitvector_typet new_type(
+      underlying_type.id(), bit_field_type.get_width());
+
+    return get_c_type(new_type);
+  }
 
   return OTHER;
 }