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] Frama-C on Linux Kernel

  • Subject: [Frama-c-discuss] Frama-C on Linux Kernel
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 18 Nov 2013 23:54:17 +0100
  • In-reply-to: <CANk9FzVcjOzbuJgKstfFxwJVt_9V9uUH6OGD+x+5UofvwT=8Xw@mail.gmail.com>
  • References: <CANk9FzVcjOzbuJgKstfFxwJVt_9V9uUH6OGD+x+5UofvwT=8Xw@mail.gmail.com>
Hello,

On Mon, Nov 18, 2013 at 11:34 PM, Qi Alfred Chen <alfchen at umich.edu> wrote:

> Hi, I am new in Frama-C, and before getting my hands dirty, I want to make
> sure that Frama-C is the best tool I need. My target is to do static
> analysis like static taint analysis, data flow analysis, etc. on Linux
> kernel code, so can anyone tell me that whether Frama-C can be successfully
> used to analyse Linux kernel code? It should be difficult due to various
> GNU extension, not sure whether Frama-C can handle that...
>

Several Linux modules have already been analyzed or are being analyzed in
Frama-C.
Indeed, Linux uses many GCCisms. Since the work on Linux modules is recent,
you would encounter some of the same bugs and limitations that have already
been encountered and fixed in the development version of Frama-C. You would
also encounter new bugs and limitations, because you wouldn't be doing
exactly the same thing that has already been done.

I should however temper the above moderate optimism by a warning: you
cannot analyze even a well-delimited Linux module as your first Frama-C
project. Even if you are familiar with Linux, you would need to have
practiced Frama-C with C programs of increasing difficulty and learned how
to use each of the available plug-ins, and how to tackle the various
difficulties that can present themselves. The good news is that while you
would be doing that, a new version would probably arrive, fixing at least
the bugs and limitations that have already been encountered.

How much time do you have to get to the point where you will be ready to
analyze (a bit of) the Linux kernel? What alternatives do you have? Do you
really need a sound static analyzer for what you ultimately intend to do,
or would it make more sense to use less demanding techniques?

Best regards,

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131118/6bedeecb/attachment.html>