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; }