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] Help, how to use Frama-C to scan linux kernel?

  • Subject: [Frama-c-discuss] Help, how to use Frama-C to scan linux kernel?
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Tue, 10 Apr 2012 17:28:29 +0200
  • In-reply-to: <CAOX9wc+x=J5C6HfYfcU7HRtTmLeuouajeSoEf5v9AenuBAe7fg@mail.gmail.com>
  • References: <CAOX9wc+x=J5C6HfYfcU7HRtTmLeuouajeSoEf5v9AenuBAe7fg@mail.gmail.com>
Hello Dana,

2012/4/10 Dana Dorneanu <dana.dorneanu at gmail.com>:
> I found this older thread and this subject[1] is very similar with something
> that I am trying to do. I am trying to generate metrics from linux kernel
> using frama-c -metrics tool.
> As suggested in this thread I compiled the kernel with the option?gcc
> -save-temps. I did this by changing in the Makefile the line
>
> CC ? ? ? ? ? ? ?= $(CROSS_COMPILE)gcc -save-temps
>
> The outcome of this was a lot of *.i and *.s files.
> Then I tried to get metrics from this files ?but I get all sorts of errors
> from the *.h files of the kernel like the following:
>
> include/linux/rcupdate.h:825:[kernel] warning: CALL in constant
> include/linux/rcupdate.h:825:[kernel] user error: 1 - 2 *
> ? ? ? ? ? ? ? ? ? ? ?!(!(!__is_kfree_rcu_offset( offset))) has side-effects
>

The location of the error is very probably due to a #line directive.
Depending on what you want to do, you might want to erase them from
the .i so that frama-c reports issues located directly in the .i
rather than in the original file (in particular, this would probably
make it easier to give minimal examples reproducing the issues). The
message you're seeing indicates likely that there's a function call in
an initializer for a static variable  (it's hard to tell for sure, as
there's not enough information in your mail to reproduce). Only
constant expressions are admissible there, which precludes function
call (see C standard, 6.7.8?4 and 6.6?3). I'd suspect that this gets
accepted by gcc because __is_kfree_rcu_offset is declared inline and
its body boils
down to returning a simple expression (again, it's hard to tell for
sure without a simple example to reproduce). If that is indeed the
case, we don't have currently enough resources to support whatever
extension gcc sees fit to implement and thus must restrict ourselves
to the project we get fundings for.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile