diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ccbe1f20c772b588235a497545701421effd9558..f6aebe306d45681b089a7e5e8c08a75260f7e139 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5503,24 +5503,21 @@ and makeCompType ghost (isstruct: bool)
match widtho with
| None -> None, ftype
| Some w -> begin
+ let source = fst w.expr_loc in
(match unrollType ftype with
| TInt (_, _) -> ()
| TEnum _ -> ()
| _ ->
- Kernel.error ~once:true ~source
+ Kernel.abort ~once:true ~source
"Base type for bitfield is not an integer type");
match isIntegerConstant ghost w with
| None ->
- Kernel.error ~source
+ Kernel.abort ~source
"bitfield width is not a valid integer constant";
- (* error does not immediately stop execution.
- Hence, we return a placeholder here.
- *)
- Some 0, ftype
| Some s as w ->
begin
if s < 0 then
- Kernel.error ~source "negative bitfield width (%d)" s;
+ Kernel.abort ~source "negative bitfield width (%d)" s;
try
if s > Cil.bitsSizeOf ftype then
Kernel.error ~source
@@ -5559,8 +5556,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/struct_with_invalid_field.0.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4babdfba70bb34026e442c04b29f88f77df5a53e
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.0.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+/* Generated by Frama-C */
+
diff --git a/tests/syntax/oracle/struct_with_invalid_field.1.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..08f35f292b14547a0bb6cb2273643c590c685e9f
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.1.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:13: User Error:
+ field `f' declared as a function
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.2.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..74ab8ae4929831eabb086c70a64621a0a51abc77
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.2.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:21: User Error:
+ negative bitfield width (-1)
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.3.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9f48a481b14d8c7fa5a5e78205a394a884da326d
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.3.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:24: User Error:
+ negative bitfield width (-2147483648)
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.4.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b1712e7f4e0211385f08c79380d7d19887ef3f4c
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.4.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing struct_with_invalid_field.c (with preprocessing)
+[kernel] struct_with_invalid_field.c:27: User Error:
+ named bitfield (d) with zero width
+[kernel] User Error: stopping on file "struct_with_invalid_field.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/struct_with_invalid_field.res.oracle b/tests/syntax/oracle/struct_with_invalid_field.res.oracle
deleted file mode 100644
index dd110c6d7c9d94c4d9dc3ef3b40edfa622c837cc..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/struct_with_invalid_field.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-[kernel] Parsing struct_with_invalid_field.i (no preprocessing)
-[kernel] struct_with_invalid_field.i:8: User Error:
- field `f' declared as a function
-[kernel] struct_with_invalid_field.i:14: User Error:
- negative bitfield width (-1)
-[kernel] struct_with_invalid_field.i:15: User Error:
- negative bitfield width (-2147483648)
-[kernel] User Error: stopping on file "struct_with_invalid_field.i" that has errors.
-[kernel] Frama-C aborted: invalid user input.
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..7e979a78da83b634c71c301194a1088e2b259f8f
--- /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:18: 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/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 070b0b0891f16262542a70f19eb56aace59d771e..1236cc7d7251b2e8c568575ebd87c1f5fe81ecbc 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -3,11 +3,6 @@
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
[kernel] very_large_integers.c:26: User Error:
bitfield width is not a valid integer constant
-[kernel] very_large_integers.c:74: Warning:
- ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:74: Warning:
- ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
- (9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/struct_with_invalid_field.c b/tests/syntax/struct_with_invalid_field.c
new file mode 100644
index 0000000000000000000000000000000000000000..527c15e35e09fab00562f15130b246cf8888b027
--- /dev/null
+++ b/tests/syntax/struct_with_invalid_field.c
@@ -0,0 +1,30 @@
+/* run.config*
+ STDOPT:
+ EXIT: 1
+ STDOPT: #"-cpp-extra-args=-DFUNTYPE"
+ STDOPT: #"-cpp-extra-args=-DNEG1"
+ STDOPT: #"-cpp-extra-args=-DNEG2"
+ STDOPT: #"-cpp-extra-args=-DNAMEDZERO"
+*/
+
+#ifdef FUNTYPE
+// invalid field with function type, parsing should fail
+struct {
+ void f(int);
+} s;
+#endif
+
+// negative-width bitfields, parsing should fail
+struct neg_bf
+{
+#ifdef NEG1
+ int a:(-1); // invalid
+#endif
+#ifdef NEG2
+ int b:(-2147483647-1); // invalid
+#endif
+#ifdef NAMEDZERO
+ int d:(-0); // invalid (named zero-width)
+#endif
+ int :(-0); // valid (unnamed zero-width)
+};
diff --git a/tests/syntax/struct_with_invalid_field.i b/tests/syntax/struct_with_invalid_field.i
deleted file mode 100644
index c1c4e15224e7da9d063a5618975c1f6c14823de1..0000000000000000000000000000000000000000
--- a/tests/syntax/struct_with_invalid_field.i
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config*
- EXIT: 1
- STDOPT:
-*/
-
-// invalid field with function type, parsing should fail
-struct {
- void f(int);
-} s;
-
-// negative-width bitfields, parsing should fail
-struct neg_bf
-{
- int a:(-1); // invalid
- int b:(-2147483647-1); // invalid
- int d:(-0); // valid
-};
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..a7de6191a45e32d95a96bfde962081c2891b47a3 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 attempt to initialize it
unsigned int control: 14, : 0;
} s_bitfield;