From c5b28669c542539c01413012fa730d4b7534f706 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 1 Sep 2021 16:38:09 +0200
Subject: [PATCH] [kernel] Do not warn anymore on FAM in GCC mode
---
src/kernel_internals/typing/cabs2cil.ml | 11 ++++-------
tests/value/oracle/empty_base.0.res.oracle | 4 ----
tests/value/oracle/fam_sizeof.res.oracle | 6 ------
tests/value/oracle/zerolengtharrays.res.oracle | 2 --
4 files changed, 4 insertions(+), 19 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a4035041d2b..e0340df0d39 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5440,17 +5440,14 @@ and makeCompType ghost (isstruct: bool)
if Cil.isFunctionType ftype then
Kernel.error ~source
"field `%s' declared as a function" n
- else if Cil.has_flexible_array_member ftype && isstruct then
- if last_group && last_field && (Cil.gccMode() || Cil.msvcMode ()) then
- Kernel.warning ~source ~once:true
- "field `%s' declared with a type containing a flexible array \
- member only allowed for GCC/MSVC."
- n
- else
+ else if Cil.has_flexible_array_member ftype && isstruct then begin
+ if not (last_group && last_field && (Cil.gccMode() || Cil.msvcMode ()))
+ then
Kernel.error ~source
"field `%s' declared with a type containing a flexible array \
member."
n
+ end
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
then begin
match Cil.unrollType ftype with
diff --git a/tests/value/oracle/empty_base.0.res.oracle b/tests/value/oracle/empty_base.0.res.oracle
index 21e946f360a..a306ba772c8 100644
--- a/tests/value/oracle/empty_base.0.res.oracle
+++ b/tests/value/oracle/empty_base.0.res.oracle
@@ -3,12 +3,8 @@
variable `c' has initializer but incomplete type
[kernel] tests/value/empty_base.c:67: Warning:
Too many initializers for structure
-[kernel] tests/value/empty_base.c:75: Warning:
- field `z' declared with a type containing a flexible array member only allowed for GCC/MSVC.
[kernel] tests/value/empty_base.c:81: User Error:
field `f1' declared with a type containing a flexible array member.
-[kernel] tests/value/empty_base.c:83: Warning:
- field `f' declared with a type containing a flexible array member only allowed for GCC/MSVC.
[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.
diff --git a/tests/value/oracle/fam_sizeof.res.oracle b/tests/value/oracle/fam_sizeof.res.oracle
index 937574dc58b..7264b646f21 100644
--- a/tests/value/oracle/fam_sizeof.res.oracle
+++ b/tests/value/oracle/fam_sizeof.res.oracle
@@ -1,10 +1,4 @@
[kernel] Parsing tests/value/fam_sizeof.i (no preprocessing)
-[kernel] tests/value/fam_sizeof.i:22: Warning:
- field `s3' declared with a type containing a flexible array member only allowed for GCC/MSVC.
-[kernel] tests/value/fam_sizeof.i:23: Warning:
- field `s2' declared with a type containing a flexible array member only allowed for GCC/MSVC.
-[kernel] tests/value/fam_sizeof.i:24: Warning:
- field `s1' declared with a type containing a flexible array member only allowed for GCC/MSVC.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/oracle/zerolengtharrays.res.oracle b/tests/value/oracle/zerolengtharrays.res.oracle
index cef0c58ef6f..64545574edd 100644
--- a/tests/value/oracle/zerolengtharrays.res.oracle
+++ b/tests/value/oracle/zerolengtharrays.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing tests/value/zerolengtharrays.i (no preprocessing)
-[kernel] tests/value/zerolengtharrays.i:7: Warning:
- field `z' declared with a type containing a flexible array member only allowed for GCC/MSVC.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
--
GitLab