diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 9e04c0ee08ba281881a96540de6bcc06c09ca328..63b72bb5aa336b8964bebb9f1a20127413b86609 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5507,28 +5507,24 @@ and makeCompType ghost (isstruct: bool)
| TInt (_, _) -> ()
| TEnum _ -> ()
| _ ->
- Kernel.error ~once:true ~source
+ Kernel.abort ~once:true ~current:true
"Base type for bitfield is not an integer type");
match isIntegerConstant ghost w with
| None ->
- Kernel.error ~source
+ Kernel.abort ~current:true
"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 ~current:true "negative bitfield width (%d)" s;
try
if s > Cil.bitsSizeOf ftype then
- Kernel.error ~source
+ Kernel.error ~current:true
"bitfield width (%d) exceeds its type (%a, %d bits)"
s Cil_printer.pp_typ ftype (Cil.bitsSizeOf ftype)
with
SizeOfError _ ->
- Kernel.fatal ~source
+ Kernel.fatal ~current:true
"Unable to compute size of %a" Cil_printer.pp_typ ftype
end;
let ftype =
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..44f758c2e5d8d9630c9058f1f041f4b8b2e5fcb4
--- /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:18: 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..b60db2046f2598184d7fc86ee722f5403d872499
--- /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:18: 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..1e059811ea2a618d20d1d96587c2897c1cd5b1be
--- /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:18: 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/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 070b0b0891f16262542a70f19eb56aace59d771e..2d2a9cccb8aa58b64d43325cda4135e660e12438 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,13 +1,8 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
[kernel] very_large_integers.c:25: User Error:
integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] very_large_integers.c:26: User Error:
+[kernel] very_large_integers.c:25: 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
-};