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