--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2016 ---
On Tue, Nov 29, 2016 at 12:41 PM, Gergö Barany <gergo.barany at cea.fr> wrote: > See if you can get your Linux configuration to avoid defining this variable, then you should be able to parse the rest of the file. Thanks Gergö. I realized the original implementation of mul_u64_u32_shr depends on CONFIG_ARCH_SUPPORTS_INT128 being defined, a necessary requirement for compiling an x64 kernel. So I recompiled a 32bit kernel and the problem is solved, but I stumbled upon another problem: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing ext2.mod.i (no preprocessing) ../../include/linux/cpumask.h:760,46:[kernel] Dropping side-effect in sizeof. Nothing to worry, this is by the book. ../.././arch/x86/include/asm/paravirt.h:407,86:[kernel] failure: typeOffset: Field func on a non-compound type 'void *' [kernel] user error: skipping file "ext2.mod.i" that has errors. [kernel] Frama-C aborted: invalid user input. I'm not sure if there's an easy altercation to overcome this one.