--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on March 2011 ---
[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