diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index e0340df0d398b77850734249581b05204f9e62aa..b4c42752be638a6b7cdd8ba9e550ce1b5208ad34 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 bb1c0f48c0786337b8a291c5d22227dca656e281..09f6142e6ee268b2a09e35a7da9a3bbe87c3c745 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 a306ba772c856402eee3316345553d942bb598d3..b98d0cf31dfbd4a81605e0ef46e047e3ca87a588 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.