From 095c403b86896058b028a8b0700a4fb16cc2e3d3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 2 Sep 2021 08:09:43 +0200
Subject: [PATCH] [kernel] Clearer error messages related to FAMs
---
src/kernel_internals/typing/cabs2cil.ml | 10 +++++++---
.../oracle/flexible_array_member_invalid5.res.oracle | 2 +-
tests/value/oracle/empty_base.0.res.oracle | 2 +-
3 files changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e0340df0d39..b4c42752be6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5441,11 +5441,15 @@ and makeCompType ghost (isstruct: bool)
Kernel.error ~source
"field `%s' declared as a function" n
else if Cil.has_flexible_array_member ftype && isstruct then begin
- if not (last_group && last_field && (Cil.gccMode() || Cil.msvcMode ()))
- then
+ if not (last_group && last_field) then
+ Kernel.error ~source
+ "non-final field `%s' declared with a type containing a flexible \
+ array member."
+ n
+ else if not (Cil.gccMode() || Cil.msvcMode ()) then
Kernel.error ~source
"field `%s' declared with a type containing a flexible array \
- member."
+ member only allowed in GCC/MSVC mode."
n
end
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
diff --git a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
index bb1c0f48c07..09f6142e6ee 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid5.i (no preprocessing)
[kernel] tests/syntax/flexible_array_member_invalid5.i:15: User Error:
- field `f' declared with a type containing a flexible array member.
+ field `f' declared with a type containing a flexible array member only allowed in GCC/MSVC mode.
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid5.i" that has
errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/empty_base.0.res.oracle b/tests/value/oracle/empty_base.0.res.oracle
index a306ba772c8..b98d0cf31df 100644
--- a/tests/value/oracle/empty_base.0.res.oracle
+++ b/tests/value/oracle/empty_base.0.res.oracle
@@ -4,7 +4,7 @@
[kernel] tests/value/empty_base.c:67: Warning:
Too many initializers for structure
[kernel] tests/value/empty_base.c:81: User Error:
- field `f1' declared with a type containing a flexible array member.
+ non-final 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.
[kernel] Frama-C aborted: invalid user input.
--
GitLab