--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Frama-C for Analyzing Linux Kernel



Hi folks,
I'm expected to do a project for a course which involves running various
static analysis tools on some Linux kernel modules — fs/ext2 module for
start. I've analyzed the code with a couple of SCATs (including SPARSE,
FlawFinder, BLAST, etc.), though my professor insisted that I also give
Frama-C a try. I was wondering if there’s been any work on using Frama-C
with Linux kernel as googling doesn’t yield much.

FYI, I have added the line "ccflags-y := -save-temps=obj" to this module's
Makefile, so the preprocessed intermediate file ext2.mod.i is generated
during compilation. Afterwards I run frama-c and pass the .i file as input,
but it prints our the error below:

[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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161129/413508e8/attachment.html>