[kernel] Clearer error messages related to FAMs

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)

tests/syntax/oracle/flexible_array_member_invalid5.res.oracle

 [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.

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.