--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2019 ---
Indeed, I don't see an explicit interdiction in the standard (and, in a more pragmatic vein, GCC/Clang accept it with `-pedantic -std=c99`, so there's at least something to be said about compatibility). I will defer it to my colleagues in case I'm mistaken, but in the meanwhile, if you can manually compile the Frama-C sources, the following patch should be enough: ------------------- src/kernel_internals/typing/cabs2cil.ml ------------------- @@ -5230,7 +5230,7 @@ and makeCompType ghost (isstruct: bool)       if Cil.isFunctionType ftype then         Kernel.error ~current:true           "field `%s' declared as a function" n -     else if Cil.has_flexible_array_member ftype then +     else if Cil.has_flexible_array_member ftype && isstruct then         Kernel.error ~current:true           "field `%s' declared with a type containing a flexible array member."           n Otherwise, if you use opam, it should be possible to make a quick branch to be used via `opam pin`. It's not much different from cloning the Frama-C Github repository, just that it will be opam doing it for you. Let me know if it interests you. On 19/08/2019 06:27, Johannes Paasila wrote: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Researcher/Engineer CEA/List Software Reliability and Security Laboratory