Fix bit-field and __CPROVER_bool padding for Visual Studio

Bit fields that sum up to the underlying type need to update the offset
to ensure padding suitable for the alignment is inserted.

Author: tautschnig

regression/ansi-c/bitfields1/main.c

@@ -0,0 +1,33 @@
+#include <limits.h>
+
+#define STATIC_ASSERT(condition) int some_array##__LINE__[(condition) ? 1 : -1]
+
+#if CHAR_BIT == 8
+struct bits
+{
+  char a : 4;
+  char b : 4;
+  char c : 4;
+  char d : 4;
+  int i;
+};
+
+STATIC_ASSERT(sizeof(struct bits) == 2 * sizeof(int));
+
+#pragma pack(1)
+struct packed_bits
+{
+  char a : 4;
+  char b : 4;
+  char c : 4;
+  char d : 4;
+  int i;
+};
+#pragma pack()
+
+STATIC_ASSERT(sizeof(struct packed_bits) == sizeof(int) + 2);
+#endif
+
+int main()
+{
+}

regression/ansi-c/bitfields1/test.desc

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

regression/ansi-c/cprover_bool1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

src/ansi-c/padding.cpp

@@ -190,6 +190,11 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
       const auto width = to_c_bit_field_type(it->type()).get_width();
       bit_field_bits += width;
     }
+    else if(
+      it->type().id() == ID_bool && underlying_bits == config.ansi_c.char_width)
+    {
+      ++bit_field_bits;
+    }
     else
     {
       // pad up any remaining bit field
@@ -201,6 +206,11 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
         offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
         underlying_bits = bit_field_bits = 0;
       }
+      else
+      {
+        offset += bit_field_bits / config.ansi_c.char_width;
+        underlying_bits = bit_field_bits = 0;
+      }
 
       // pad up to underlying type unless the struct is packed
       if(!is_packed)
@@ -231,6 +241,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
       }
       else if(it->type().id() == ID_bool)
       {
+        underlying_bits = config.ansi_c.char_width;
         ++bit_field_bits;
       }
       else
@@ -252,6 +263,8 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
     pad_bit_field(components, components.end(), pad);
     offset += (bit_field_bits + pad) / config.ansi_c.char_width;
   }
+  else
+    offset += bit_field_bits / config.ansi_c.char_width;
 
   // alignment of the struct
   // Note that this is done even if the struct is packed.