diff --git a/regression/cbmc/Bitfields1/main.c b/regression/cbmc/Bitfields1/main.c index 7ab19426ca3..147b1299100 100644 --- a/regression/cbmc/Bitfields1/main.c +++ b/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); } 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$