Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Struct with flexible array member within union
  • From: mail at jonne.org (Johannes Paasila)
  • Date: Mon, 19 Aug 2019 14:27:31 +1000
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