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: Andre.MARONEZE at cea.fr (Andre Maroneze)
  • Date: Wed, 21 Aug 2019 09:09:34 +0200
  • In-reply-to: <877e79hj9o.fsf@jonne.org>
  • References: <877e79hj9o.fsf@jonne.org>
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