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