--- layout: fc_discuss_archives title: Message 22 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 28/11/16 22:50, Nima Mohammadi wrote:
> [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no
> preprocessing)
> [kernel] Parsing ext2.mod.i (no preprocessing)
> ../../include/linux/math64.h:141,0:[kernel] user error: syntax error
> [kernel] user error: stopping on file "ext2.mod.i" that has errors.
> [kernel] Frama-C aborted: invalid user input.
>
> I'm not sure what the next step should be. I increased the verbosity of
> frama-c, but still didn't get a better description of what had gone
> wrong. Any thoughts?

On my system, line 141 of
/usr/src/linux-headers-4.4.0-45/include/linux/math64.h is:

     return (u64)(((unsigned __int128)a * mul) >> shift);

The syntax error seems to be due to the __int128 type, which is not 
supported by Frama-C.

A few lines above this there is the following guard:

#if defined(CONFIG_ARCH_SUPPORTS_INT128) && defined(__SIZEOF_INT128__)

and there is an alternative implementation of the operations in question 
that does not use __int128. 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.


Hope this helps,
Gergö