--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Frama-C for Analyzing Linux Kernel



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.