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