--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2016 ---
The following program shows the same behavior: struct paravirt_callee_save { void *func; }; struct pv_mmu_ops { struct paravirt_callee_save make_pte; }; extern struct pv_mmu_ops pv_mmu_ops; int main() { pv_mmu_ops.make_pte.func; } We'll take a look at it to see if Frama-C is being too strict. On a side note, for future code posting, using another website such as Github Gist might be helpful. Ubuntu pastebin requires a login just to be able to download the text-only version... On 01/12/2016 03:15, Nima Mohammadi wrote: > Installed Silicium-rc1, but I still get the same error message. > This is the preprocessed source ext2.mod.i, if you're interested: > http://paste.ubuntu.com/23560908/ > > On Wed, Nov 30, 2016 at 12:58 PM, Gergö Barany <gergo.barany at cea.fr > <mailto:gergo.barany at cea.fr>> wrote: > > On 29/11/16 21:11, Nima Mohammadi wrote: > > ../.././arch/x86/include/asm/paravirt.h:407,86:[kernel] failure: > typeOffset: Field func on a non-compound type 'void *' > > > This looks strange. You could see if it's a bug in your version of > Frama-C that's fixed in the Silicium/Silicon release snapshot at > https://github.com/Frama-C/Frama-C-snapshot/releases > <https://github.com/Frama-C/Frama-C-snapshot/releases> > > If not, it's probably impossible to say much more without the > preprocessed source you are trying to parse. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > <http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss> > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Ingénieur-chercheur CEA/LIST Laboratoire Sûreté et Sécurité des Logiciels -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161201/42a03294/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3797 bytes Desc: S/MIME Cryptographic Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161201/42a03294/attachment.bin>