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/cprover_bool1/test.desc

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

src/ansi-c/padding.cpp

@@ -190,6 +190,12 @@ 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 +207,8 @@ 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 += underlying_bits / config.ansi_c.char_width;
 
       // pad up to underlying type unless the struct is packed
       if(!is_packed)
@@ -231,6 +239,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 +261,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 += underlying_bits / config.ansi_c.char_width;
 
   // alignment of the struct
   // Note that this is done even if the struct is packed.