diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4e618d714d3fd4976b3432c1ae018338825cf393..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 ~source:(fst cloc)
+ Kernel.error ~once:true ~source
"Base type for bitfield is not an integer type");
match isIntegerConstant ghost w with
| None ->
- Kernel.error ~source:(fst cloc)
+ Kernel.error ~source
"bitfield width is not an integer constant";
(* error does not immediately stop execution.
Hence, we return a placeholder here.
@@ -5477,15 +5478,15 @@ and makeCompType ghost (isstruct: bool)
| Some s as w ->
begin
if s < 0 then
- Kernel.error ~source:(fst cloc) "negative bitfield width (%d)" s;
+ Kernel.error ~source "negative bitfield width (%d)" s;
try
if s > Cil.bitsSizeOf ftype then
- Kernel.error ~source:(fst cloc)
+ 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 ~source:(fst cloc)
+ 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
index b54f3ab0368599cabc43276115e2a317bae3dfa8..53e414a962088f221e56cfc8d54ffc5c7c53eedb 100644
--- a/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
+++ b/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/struct_with_function_field_invalid.i (no preprocessing)
-[kernel] tests/syntax/struct_with_function_field_invalid.i:7: User Error:
+[kernel] tests/syntax/struct_with_function_field_invalid.i:8: 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.
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.