Merge pull request #3713 from diffblue/bitfield-promotion

test for bitfield promotion

Author: tautschnig

regression/cbmc/Bitfields1/main.c

@@ -8,10 +8,10 @@ typedef enum _INTEL_CACHE_TYPE {
 } INTEL_CACHE_TYPE;
 
 struct bft {
-  unsigned int a:3;
+  unsigned long int a : 3;
   unsigned int b:1;
   signed int c:2;
-  _Bool d:3;
+  _Bool d : 1;
 
   // an anonymous bitfield
   signed int :2;
@@ -20,7 +20,7 @@ struct bft {
   INT x:1;
 
   // made of sizeof
-  unsigned int abc: sizeof(int);
+  unsigned int abc : sizeof(int) * 8;
 
   // enums are integers!
   INTEL_CACHE_TYPE Type : 5;
@@ -53,7 +53,14 @@ int main() {
 
   // assignments have the underlying type
   assert(sizeof(bf.d=1)==sizeof(_Bool));
-  assert(sizeof(bf.a+=1)==sizeof(unsigned));
+  assert(sizeof(bf.a += 1) == sizeof(unsigned long));
 
   bf.Type=IntelCacheTrace;
+
+  // promotion rules apply, and thus, bf.a is signed,
+  // but bf.abc is unsigned
+  bf.a = 0;
+  assert(bf.a - 1 < 0);
+  bf.abc = 0;
+  assert(bf.abc - 1 >= 0);
 }

regression/cbmc/Bitfields1/test.desc

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