--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on April 2012 ---
[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?



Dear all,

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 commands I used for trying this are:
For example:

frama-c -metrics ipw2200.mod.i
frama-c -metrics framac_preprocessing/*.i
frama-c -continue-annot-error framac_preprocessing/*.i

I tried a similar thing with a much simpler program and everything worked
smooth.

If you managed to do this could you give a hint to get out of from this
blockage?

thanks a lot.

[1]
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-March/002597.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120410/7d637ba0/attachment.html>