Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Using Frama-C for Analyzing Linux Kernel
  • From: nima.mohammadi at ut.ac.ir (Nima Mohammadi)
  • Date: Tue, 29 Nov 2016 01:20:33 +0330
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>