From 72ce0f64d73b8ee87d63b41ea315426df1eafe38 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 18 May 2021 12:25:00 +0200
Subject: [PATCH] [kernel] Cabs2cil: improves location in error messages about
struct fields.
---
src/kernel_internals/typing/cabs2cil.ml | 21 ++++++++++---------
tests/syntax/oracle/fam.res.oracle | 2 +-
.../flexible_array_member_invalid1.res.oracle | 2 +-
.../flexible_array_member_invalid2.res.oracle | 2 +-
.../flexible_array_member_invalid3.res.oracle | 2 +-
.../flexible_array_member_invalid4.res.oracle | 2 +-
.../flexible_array_member_invalid5.res.oracle | 2 +-
.../oracle/incomplete_struct_field.res.oracle | 2 +-
...uct_with_function_field_invalid.res.oracle | 2 +-
tests/value/oracle/empty_base.0.res.oracle | 2 +-
10 files changed, 20 insertions(+), 19 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4e618d714d3..4e88edb64f0 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 8ccf9f18f6f..cd389c848e2 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 1747cd9c2c3..9946bb6acd8 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 08b2bbe1285..99f1f24d882 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 c7e88ab0629..b344417d741 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 238b92acd43..d2876944dca 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 8e1dca203f5..bb1c0f48c07 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 1fd54ec0cfd..893450fdd3c 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 b54f3ab0368..53e414a9620 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 0af48095560..28a0b5e21ea 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.
--
GitLab