Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.