diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index a4035041d2bbe7947fe436eb0353f4c3703f1fb2..e0340df0d398b77850734249581b05204f9e62aa 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 21e946f360ab13b7a9879cb075ed54d52ea41d0d..a306ba772c856402eee3316345553d942bb598d3 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 937574dc58ba303186061527b84a1f9c174b5d88..7264b646f21985e58e5ad713b31d3834b6b6a5bf 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 cef0c58ef6fb33e2d45ce0d5b7bf712236895c43..64545574edd106ecd547443e37723db0060d3d18 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