--- layout: fc_discuss_archives title: Message 6 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



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