--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2019 ---
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