diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index ccbe1f20c772b588235a497545701421effd9558..9e04c0ee08ba281881a96540de6bcc06c09ca328 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -5559,8 +5559,12 @@ and makeCompType ghost (isstruct: bool) anonCompFieldName ^ (string_of_int !anonCompFieldNameId) end | _ -> n - end else + end else begin + if fbitfield = Some 0 then + Kernel.error ~source:(fst cloc) + "named bitfield (%s) with zero width" n; n + end in let rec is_circular t = match Cil.unrollType t with diff --git a/tests/syntax/oracle/unnamed_bitfields.0.res.oracle b/tests/syntax/oracle/unnamed_bitfields.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6df296791c5eceade728f06428a3bac31f330470 --- /dev/null +++ b/tests/syntax/oracle/unnamed_bitfields.0.res.oracle @@ -0,0 +1 @@ +[kernel] Parsing unnamed_bitfields.c (with preprocessing) diff --git a/tests/syntax/oracle/unnamed_bitfields.1.res.oracle b/tests/syntax/oracle/unnamed_bitfields.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6a2d6755f07d2ab66cadfca255217ee9fcb50a8c --- /dev/null +++ b/tests/syntax/oracle/unnamed_bitfields.1.res.oracle @@ -0,0 +1,6 @@ +[kernel] Parsing unnamed_bitfields.c (with preprocessing) +[kernel] unnamed_bitfields.c:15: User Error: + named bitfield (zero_with_name) with zero width +[kernel] User Error: stopping on file "unnamed_bitfields.c" that has errors. Add + '-kernel-msg-key pp' for preprocessing command. +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/unnamed_bitfields.res.oracle b/tests/syntax/oracle/unnamed_bitfields.res.oracle deleted file mode 100644 index 89cfeea2854f55cd70a8c0554f5bdccfaf2bb952..0000000000000000000000000000000000000000 --- a/tests/syntax/oracle/unnamed_bitfields.res.oracle +++ /dev/null @@ -1,18 +0,0 @@ -[kernel] Parsing unnamed_bitfields.i (no preprocessing) -/* Generated by Frama-C */ -struct foo { - unsigned int bar : 16 ; - unsigned int : 0 ; - unsigned int bla : 11 ; - unsigned int : 1 ; - unsigned int bli : 4 ; - unsigned int : 0 ; -}; -unsigned int f(struct foo s) -{ - unsigned int __retres; - __retres = (unsigned int)s.bla; - return __retres; -} - - diff --git a/tests/syntax/unnamed_bitfields.c b/tests/syntax/unnamed_bitfields.c new file mode 100644 index 0000000000000000000000000000000000000000..6f999ad0a8ac91bca35a22d9ce50cf2cbc3b9a7a --- /dev/null +++ b/tests/syntax/unnamed_bitfields.c @@ -0,0 +1,23 @@ +/* run.config +OPT: +EXIT:1 +OPT: -cpp-extra-args="-DINVALID_ZERO_BF" + */ + +struct foo +{ + unsigned bar : 16, : 0; + unsigned bla : 11, : 1; + unsigned bli : 4, : 0; +}; + +#ifdef INVALID_ZERO_BF +struct invalid_foo +{ + unsigned first : 1; + unsigned zero_with_name: 0; + unsigned last : 2; +}; +#endif + +unsigned f(struct foo s) { return s.bla; } diff --git a/tests/syntax/unnamed_bitfields.i b/tests/syntax/unnamed_bitfields.i deleted file mode 100644 index 14e793c74ab38cbe87329bc9f89ec5693c4584a4..0000000000000000000000000000000000000000 --- a/tests/syntax/unnamed_bitfields.i +++ /dev/null @@ -1,8 +0,0 @@ -struct foo -{ - unsigned bar : 16, : 0; - unsigned bla : 11, : 1; - unsigned bli : 4, : 0; -}; - -unsigned f(struct foo s) { return s.bla; } diff --git a/tests/value/library.i b/tests/value/library.i index 797623ff33b77cc4ee483367070e4bf42c3cf926..8a05e15874684493bbaa0d8ea10a1ef561044460 100644 --- a/tests/value/library.i +++ b/tests/value/library.i @@ -60,7 +60,7 @@ void (*ff)(); struct { short bf1: 5; - short bf : 0; // 0-sized bitfield: do not attemp to initialize it + short : 0; // 0-sized bitfield: do not attemp to initialize it unsigned int control: 14, : 0; } s_bitfield;