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] Help, how to use Frama-C to scan linux kernel?

Hello, and thanks for your interest.

On Tue, Mar 29, 2011 at 9:41 AM, Zhao, Passion <passion.zhao at intel.com> wrote:
> I install the frama-c 1.4 in Fedora 12, try to use it to scan some open
> source projects such as openssl, linux.

If scanning the source files with the purpose of finding some bugs is your goal,
Frama-C is not the best tool. It is intended for verification, which
generally means
an already delimited set of functions, and some pre-existing specifications.

The distributed plug-ins are all for sequential code, so Linux is out unless you
are willing to do the work of insulating some files inside it that can are worth
analyzing in a sequential context. OpensSSL needs some of the same treatment
but it would be faster and more rewarding.

I would, like David, recommend Frama-C's value analysis because
it can be used relatively automatically (for a verification tool, that is).
The tutorial is at http://frama-c.com/download/frama-c-value-analysis.pdf .
It continues in the blog: http://blog.frama-c.com/ .
Simple uses of the value analysis require no intervention at all.
The command-line can be as simple as David showed
(however, you do not need to list *.h files on the command-line:
they are included into *.c files by pre-processing (which is applied
by Frama-C). For more sophisticated uses, you would typically
write an "analysis context" in C.

You could also investigate deductive verification, for instance with the
Jessie plug-in: http://frama-c.com/jessie.html . In this case the verification
can be done function by function, but you need to write pre-conditions and
post-conditions in the spirit of Design by Contract, and in a dedicated
language, ACSL: http://frama-c.com/acsl_tutorial_index.html .

Pascal