--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2019 ---
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