--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2016 ---
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>