From 9213145d87781a72adc3da190f1396358c326e29 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 8 Jan 2019 08:47:30 +0000
Subject: [PATCH 1/2] Enable compilation of test with gcc/clang

gcc/clang reject bit-fields with bit-width larger than the underlying type.
This change enables compilation of the test with gcc/clang.
---
 regression/cbmc/Bitfields1/main.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/cbmc/Bitfields1/main.c b/regression/cbmc/Bitfields1/main.c
index 7ab19426ca3..75d461dba9a 100644
--- a/regression/cbmc/Bitfields1/main.c
+++ b/regression/cbmc/Bitfields1/main.c
@@ -11,7 +11,7 @@ struct bft {
   unsigned int a:3;
   unsigned int b:1;
   signed int c:2;
-  _Bool d:3;
+  _Bool d : 1;
 
   // an anonymous bitfield
   signed int :2;

From 935a2ebab84669151e438783f44c5769ed9a911c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 8 Jan 2019 08:46:01 +0000
Subject: [PATCH 2/2] 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.
---
 regression/cbmc/Bitfields1/main.c    | 13 ++++++++++---
 regression/cbmc/Bitfields1/test.desc |  2 +-
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/regression/cbmc/Bitfields1/main.c b/regression/cbmc/Bitfields1/main.c
index 75d461dba9a..147b1299100 100644
--- a/regression/cbmc/Bitfields1/main.c
+++ b/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);
 }
diff --git a/regression/cbmc/Bitfields1/test.desc b/regression/cbmc/Bitfields1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Bitfields1/test.desc
+++ b/regression/cbmc/Bitfields1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$