Use extractbits to extract non-byte-fields from unions

regression/cbmc/Bitfields5/main.c

@@ -0,0 +1,10 @@
+union
+{
+  unsigned five : 5;
+  char *a;
+  unsigned one : 1;
+} b = {8};
+int main()
+{
+  __CPROVER_assert(0, "");
+}

regression/cbmc/Bitfields5/test.desc

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

src/goto-programs/rewrite_union.cpp

@@ -12,8 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include "rewrite_union.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_code.h>
@@ -85,8 +87,20 @@ void rewrite_union(exprt &expr)
 
     if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
     {
-      exprt offset = from_integer(0, c_index_type());
-      expr = make_byte_extract(op, offset, expr.type());
+      if(
+        expr.type().id() != ID_c_bit_field ||
+        to_c_bit_field_type(expr.type()).get_width() %
+            config.ansi_c.char_width ==
+          0)
+      {
+        exprt offset = from_integer(0, c_index_type());
+        expr = make_byte_extract(op, offset, expr.type());
+      }
+      else
+      {
+        const auto upper = to_c_bit_field_type(expr.type()).get_width() - 1;
+        expr = extractbits_exprt(op, upper, 0, expr.type());
+      }
     }
   }
   else if(expr.id()==ID_union)

src/goto-symex/field_sensitivity.cpp

@@ -9,8 +9,10 @@ Author: Michael Tautschnig
 #include "field_sensitivity.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
@@ -419,14 +421,24 @@ void field_sensitivityt::field_assignments_rec(
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(const auto &comp : components)
     {
-      const exprt member_rhs = apply(
-        ns,
-        state,
-        simplify_opt(
-          make_byte_extract(
-            ssa_rhs, from_integer(0, c_index_type()), comp.type()),
-          ns),
-        false);
+      exprt extract;
+      if(
+        comp.type().id() != ID_c_bit_field ||
+        to_c_bit_field_type(comp.type()).get_width() %
+            config.ansi_c.char_width ==
+          0)
+      {
+        extract = make_byte_extract(
+          ssa_rhs, from_integer(0, c_index_type()), comp.type());
+      }
+      else
+      {
+        const auto upper = to_c_bit_field_type(comp.type()).get_width() - 1;
+        extract = extractbits_exprt(ssa_rhs, upper, 0, comp.type());
+      }
+
+      const exprt member_rhs =
+        apply(ns, state, simplify_opt(extract, ns), false);
 
       const exprt &member_lhs = *fs_it;
       if(

src/util/format_type.cpp

@@ -115,6 +115,8 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
     os << u8" \u2192 "; // → -- we don't use ⟶  since that doesn't render well
     return os << format(mathematical_function.codomain());
   }
+  else if(id == ID_c_bit_field)
+    return os << "c_bit_field[" << to_c_bit_field_type(type).get_width() << ']';
   else
     return os << id;
 }