Frama-C-discuss mailing list archives

passion.zhao at intel.com (Zhao, Passion) · Wed, 30 Mar 2011 16:53:21 +0800

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"\"
-D_GNU_SOURCE -D_LARGEFILE64_SOURCE -D_FILE_OFFSET_BITS=64   -Wall  -g -O2'
./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
frama-c? 
And is there any method to feed these pre-processed files to frama-c to
analysis?
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 lists.gforge.inria.fr
[mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal
Cuoq
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
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

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 7196 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110330/3a551e9f/attachment.bin>

Frama-C-discuss mailing list archives

[Frama-c-discuss] Help, how to use Frama-C to scan linux kernel?