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