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

  • Subject: [Frama-c-discuss] Using Frama-C for Analyzing Linux Kernel
  • From: gergo.barany at cea.fr (Gergö Barany)
  • Date: Tue, 29 Nov 2016 10:11:21 +0100
  • In-reply-to: <CAPpMX7TdN7-sQ35pv47jPymQ7UWfXaH2-WXJZ3v=y6+9bCJwgA@mail.gmail.com>
  • References: <CAPpMX7TdN7-sQ35pv47jPymQ7UWfXaH2-WXJZ3v=y6+9bCJwgA@mail.gmail.com>
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ö