Fixing member offset computation in presence of bitfields

Author: marek-trtik

regression/cbmc/Bitfields3/main.c

@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+struct A {
+  unsigned char a;
+  unsigned char b:2;
+  unsigned char c:2;
+} __attribute__((packed));
+
+int main(void)
+{
+  struct A *p;
+  p = malloc(2);
+  p->c = 3;
+  if (p->c != 3) {
+    free(p);
+  }
+  free(p);
+}

regression/cbmc/Bitfields3/test.desc

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

src/util/pointer_offset_size.cpp

@@ -287,13 +287,15 @@ exprt member_offset_expr(
     if(it->type().id()==ID_c_bit_field)
     {
       std::size_t w=to_c_bit_field_type(it->type()).get_width();
+      bit_field_bits += w;
       std::size_t bytes;
-      for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
-      bit_field_bits-=w;
+      bytes = bit_field_bits / 8;
+      bit_field_bits = bit_field_bits % 8;
       result=plus_exprt(result, from_integer(bytes, result.type()));
     }
     else
     {
+      bit_field_bits = 0;
       const typet &subtype=it->type();
       exprt sub_size=size_of_expr(subtype, ns);
       if(sub_size.is_nil())