diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4282f0e9f46d53aee4dc7b2f52b9773606f1a9bc..4e88edb64f0ffd77e8db0f1dc49f208b0e94263c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5417,8 +5417,9 @@ and makeCompType ghost (isstruct: bool)
let addFieldInfo ~last:last_field (flds : fieldinfo list)
(((n,ndt,a,cloc) : A.name), (widtho : A.expression option))
: fieldinfo list =
+ let source = fst cloc in
if sto <> NoStorage || inl then
- Kernel.error ~once:true ~current:true "Storage or inline not allowed for fields";
+ Kernel.error ~once:true ~source "Storage or inline not allowed for fields";
let allowZeroSizeArrays = true in
let ftype, fattr =
doType
@@ -5431,10 +5432,10 @@ and makeCompType ghost (isstruct: bool)
struct C2 { struct C1 c1; int dummy; };
*)
if Cil.isFunctionType ftype then
- Kernel.error ~current:true
+ Kernel.error ~source
"field `%s' declared as a function" n
else if Cil.has_flexible_array_member ftype && isstruct then
- Kernel.error ~current:true
+ Kernel.error ~source
"field `%s' declared with a type containing a flexible array member."
n
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
@@ -5445,14 +5446,14 @@ and makeCompType ghost (isstruct: bool)
(* possible flexible array member; check if struct contains at least
one other field *)
if flds = [] then (* struct is empty *)
- Kernel.error ~current:true
+ Kernel.error ~source
"flexible array member '%s' (type %a) \
not allowed in otherwise empty struct"
n Cil_printer.pp_typ ftype
else (* valid flexible array member *) ()
end
| _ ->
- Kernel.error ~current:true
+ Kernel.error ~source
"field `%s' is declared with incomplete type %a"
n Cil_printer.pp_typ ftype
end;
@@ -5464,11 +5465,11 @@ and makeCompType ghost (isstruct: bool)
| TInt (_, _) -> ()
| TEnum _ -> ()
| _ ->
- Kernel.error ~once:true ~current:true
+ Kernel.error ~once:true ~source
"Base type for bitfield is not an integer type");
match isIntegerConstant ghost w with
| None ->
- Kernel.error ~current:true
+ Kernel.error ~source
"bitfield width is not an integer constant";
(* error does not immediately stop execution.
Hence, we return a placeholder here.
@@ -5476,14 +5477,16 @@ and makeCompType ghost (isstruct: bool)
Some 0, ftype
| Some s as w ->
begin
+ if s < 0 then
+ Kernel.error ~source "negative bitfield width (%d)" s;
try
if s > Cil.bitsSizeOf ftype then
- Kernel.error ~current:true
+ Kernel.error ~source
"bitfield width (%d) exceeds its type (%a, %d bits)"
s Cil_printer.pp_typ ftype (Cil.bitsSizeOf ftype)
with
SizeOfError _ ->
- Kernel.fatal ~current:true
+ Kernel.fatal ~source
"Unable to compute size of %a" Cil_printer.pp_typ ftype
end;
let ftype =
diff --git a/tests/syntax/oracle/fam.res.oracle b/tests/syntax/oracle/fam.res.oracle
index 8ccf9f18f6f5ea030a3ff85f5e597a43aa74de04..cd389c848e28e89b9b19cbf7327dc2be09f0896a 100644
--- a/tests/syntax/oracle/fam.res.oracle
+++ b/tests/syntax/oracle/fam.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/fam.i (no preprocessing)
[kernel] tests/syntax/fam.i:16: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] tests/syntax/fam.i:28: User Error:
+[kernel] tests/syntax/fam.i:29: User Error:
field `b' is declared with incomplete type char []
[kernel] tests/syntax/fam.i:28: User Error:
static initialization of flexible array members is an unsupported GNU extension
diff --git a/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle
index 1747cd9c2c39144829c5697e1846f8828161ae67..9946bb6acd85b78e0ab036576a152b97562e4371 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid1.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid1.i:7: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid1.i:8: User Error:
flexible array member 'data' (type char []) not allowed in otherwise empty struct
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid1.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle
index 08b2bbe1285519910ffd0194603ecffc25ea179d..99f1f24d88212f4b315c0b278fc9843752526173 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid2.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid2.i:7: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid2.i:9: User Error:
field `data' is declared with incomplete type char []
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid2.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle
index c7e88ab06296193f8a930b30f4ac9686c457763b..b344417d741e8e115408dae13758ce18d4b1a13d 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid3.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid3.i:8: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid3.i:10: User Error:
field `data' is declared with incomplete type char []
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid3.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle
index 238b92acd43a45da575a026a1ed434bdc0f90033..d2876944dca7cfac4bc276286000748b34f89d2d 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid4.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid4.i:7: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid4.i:9: User Error:
field `data' is declared with incomplete type char []
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid4.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
index 8e1dca203f55c5b1536d845e7f3cb4826cac798d..bb1c0f48c0786337b8a291c5d22227dca656e281 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid5.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid5.i:13: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid5.i:15: User Error:
field `f' declared with a type containing a flexible array member.
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid5.i" that has
errors.
diff --git a/tests/syntax/oracle/incomplete_struct_field.res.oracle b/tests/syntax/oracle/incomplete_struct_field.res.oracle
index 1fd54ec0cfd8ceb5a376b144f885cb2f48cc6043..893450fdd3c9ea83912a6b69431a42f8def2fdbc 100644
--- a/tests/syntax/oracle/incomplete_struct_field.res.oracle
+++ b/tests/syntax/oracle/incomplete_struct_field.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/incomplete_struct_field.i (no preprocessing)
[kernel] tests/syntax/incomplete_struct_field.i:5: User Error:
declaration of array of incomplete type 'struct _s`
-[kernel] tests/syntax/incomplete_struct_field.i:5: User Error:
+[kernel] tests/syntax/incomplete_struct_field.i:7: User Error:
field `v' is declared with incomplete type struct _s [12]
[kernel] tests/syntax/incomplete_struct_field.i:5: User Error:
type struct _s is circular
diff --git a/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle b/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
deleted file mode 100644
index b54f3ab0368599cabc43276115e2a317bae3dfa8..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-[kernel] Parsing tests/syntax/struct_with_function_field_invalid.i (no preprocessing)
-[kernel] tests/syntax/struct_with_function_field_invalid.i:7: User Error:
- field `f' declared as a function
-[kernel] User Error: stopping on file "tests/syntax/struct_with_function_field_invalid.i" that has
- errors.
-[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
new file mode 100644
index 0000000000000000000000000000000000000000..001273c4d944b386ae86f8966d5b5a9b0f613107
--- /dev/null
+++ b/tests/syntax/oracle/struct_with_invalid_field.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing tests/syntax/struct_with_invalid_field.i (no preprocessing)
+[kernel] tests/syntax/struct_with_invalid_field.i:8: User Error:
+ field `f' declared as a function
+[kernel] tests/syntax/struct_with_invalid_field.i:14: User Error:
+ negative bitfield width (-1)
+[kernel] tests/syntax/struct_with_invalid_field.i:15: User Error:
+ negative bitfield width (-2147483648)
+[kernel] User Error: stopping on file "tests/syntax/struct_with_invalid_field.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/struct_with_function_field_invalid.i b/tests/syntax/struct_with_function_field_invalid.i
deleted file mode 100644
index c522453305f94cfd11edab28d158226619f875f7..0000000000000000000000000000000000000000
--- a/tests/syntax/struct_with_function_field_invalid.i
+++ /dev/null
@@ -1,9 +0,0 @@
-/* run.config*
- EXIT: 1
- STDOPT:
-*/
-
-// invalid field with function type, parsing should fail
-struct {
- void f(int);
-} s;
diff --git a/tests/syntax/struct_with_invalid_field.i b/tests/syntax/struct_with_invalid_field.i
new file mode 100644
index 0000000000000000000000000000000000000000..c1c4e15224e7da9d063a5618975c1f6c14823de1
--- /dev/null
+++ b/tests/syntax/struct_with_invalid_field.i
@@ -0,0 +1,17 @@
+/* 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/value/oracle/empty_base.0.res.oracle b/tests/value/oracle/empty_base.0.res.oracle
index 0af48095560b9c93b62c891c7466ad21314f60a8..28a0b5e21ea980b8fd9891b1cde2b3d580e9cd31 100644
--- a/tests/value/oracle/empty_base.0.res.oracle
+++ b/tests/value/oracle/empty_base.0.res.oracle
@@ -5,7 +5,7 @@
Too many initializers for structure
[kernel] tests/value/empty_base.c:75: User Error:
field `z' declared with a type containing a flexible array member.
-[kernel] tests/value/empty_base.c:80: User Error:
+[kernel] tests/value/empty_base.c:81: User Error:
field `f1' declared with a type containing a flexible array member.
[kernel] User Error: stopping on file "tests/value/empty_base.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.