--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Struct with flexible array member within union



Hi,


I'm attempting to work with some code which includes a type definition
of a union containing structs which have flexible array members.

Frama-C rejects this, but as far as I can tell, it is valid C99.

I'm using Frama-C 19.0 (Potassium).

Here's a minimal input to reproduce the behaviour:

       typedef union {
               struct {
                      int a;
                      char vlen[];
               } b;
       } c;


Frama-C gives the following output:

        [kernel] Parsing test.c (with preprocessing)
        [kernel] test.c:1: User Error:
          field `b' declared with a type containing a flexible array
          member.
        [kernel] User Error: stopping on file "test.c" that has
          errors. Add '-kernel-msg-key pp' for preprocessing command.
        [kernel] Frama-C aborted: invalid user input.


As far as I can tell, a struct containing a flexible array member can be
a member of a union.

C99 §6.7.2.1 paragraph 2 states:

       A structure or union shall not contain a member with incomplete
       or function type (hence, a structure shall not contain an
       instance of itself, but may contain a pointer to an instance of
       itself), except that the last member of a structure with more
       than one named member may have incomplete array type; such a
       structure (and any union containing, possibly recursively, a
       member that is such a structure) shall not be a member of a
       structure or an element of an array.


This prohibits nesting a struct with a flexible array member within
another struct, but implies that a struct with a flexible array member
can be a member of a union.

Am I correct in believing such a definition should be accepted by
Frama-C? Is there a way I can get Frama-C to accept the input?


Many thanks,

--
Johannes