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?

  • Subject: [Frama-c-discuss] Help, how to use Frama-C to scan linux kernel?
  • From: passion.zhao at (Zhao, Passion)
  • Date: Wed, 30 Mar 2011 16:53:21 +0800
  • In-reply-to: <>
  • References: <> <> <>

Hi, David and Pascal

Really appreciate your suggestion and help :) 

Now I can scan cryptsetup using frama-c-Carbon-20110201 on Fedora12.
The command line is:
frama-c-gui -val -cpp-command 'gcc -C -E -DHAVE_CONFIG_H -I. -Ilib -Isrc
-Iluks -DDATADIR=\""/usr/share"\" -DLIBDIR=\""/usr/lib"\"
-DPREFIX=\""/usr"\" -DSYSCONFDIR=\""/etc"\" -DVERSION=\""1.1.0"\"
./luks/*.c lib/*.c src/*.c

But to scan more complicate project, it is still difficult to pass long file
list and various compiler parameters to -cpp-command.
Can we base on the default building to generate the pre-processed files for
And is there any method to feed these pre-processed files to frama-c to
I believe if there is such generic method, we can use frama-c to scan any
complicate project easily.

Any suggestions? Thanks.

Best regards,
- Passion
iNet: 8751-1986

-----Original Message-----
From: frama-c-discuss-bounces at
[mailto:frama-c-discuss-bounces at] On Behalf Of Pascal
Sent: Tuesday, March 29, 2011 6:32 PM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] Help, how to use Frama-C to scan linux

Hello, and thanks for your interest.

On Tue, Mar 29, 2011 at 9:41 AM, Zhao, Passion <passion.zhao at>
> 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

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 .
It continues in the blog: .
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: . 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: .


Frama-c-discuss mailing list
Frama-c-discuss at
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 7196 bytes
Desc: not available
URL: <>