test for bit-field promotion (#3709)

Usual promotion rules apply to bit-fields -- thus, an unsigned bit-field
that is smaller than 'int' gets promoted to 'int', and thus yields a signed
expression. Issue #3709.

Author: Daniel Kroening

regression/cbmc/Bitfields1/main.c

@@ -8,7 +8,7 @@ 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 : 1;
@@ -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$