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



Andre,


Many thanks for your response.


> 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


With this patch in place, Frama-C successfully accepts my code.


Cheers!


--
Johannes