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] long and complex program

Hello,

I have just started a new project to verify a C code using Frama C. I am facing so much problems.
Is it a good idea to verify a long and so complex C code using Frama C (jessie plug in)?
Could you answer me, please?
Could you share your experience?

Best regards,
Intissar




________________________________
 De?: Boris Yakobowski <boris at yakobowski.org>
??: prubel at bbn.com; Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> 
Envoy? le : Mercredi 2 janvier 2013 20h27
Objet?: Re: [Frama-c-discuss] value analysis and system calls
 

Hello,



On Tue, Oct 16, 2012 at 8:58 PM, Paul Rubel <prubel at bbn.com> wrote:

I also tried to pull in the files/functions from the frama-c/libc/
>directory piecemeal but ended up in a similar situation, some
>definitions don't seem to have annotations on them or implementations,
>such as open or dup2. I understand that I can go through and annotate
>each function by hand, but I feel like I must be missing something or
>doing work that other folks have already done when I annotate standard
>calls. What am I missing something?
>
?
Are there examples out there of programs that make use of a fair
>number of system calls being sliced or analyzing cleanly?
>

To answer your last question first, yes, but not immediately. Value Analysis and Slicing both require a properly stubbed code, regardless of the number of missing functions. All the big programs that were successfully analyzed using Value were either embedded ones (with a very restricted, supplied, standard library), or were using few system calls. In this last case, all the important library functions had to be stubbed or specified manually. 


Regarding POSIX programs, Frama-C's standard library has been under constant development from one release to another. Specifications or bodies for new functions appear with each new version (in the share/libc directory). Still, this is an often tedious task, is not directly related to research, and has not been required by industrials so far. Thus, unless someones steps in with some specifications for some functions (that we will gladly incorporate), some manpower for this task, or some funds dedicated to this, the improvements are likely to remain gradual.

To conclude, this addresses mainly the functions that can be specified in ACSL in the fragment that can be understood by Value (or with only reasonable extensions). Functions that use malloc must be checked for use-after-free, double 
free, etc. Similarly, open/close calls must be verified for absence of memory leak, of double close, etc. This is tricky to specify, but also to verify. Devising a proper abstraction that 
remains fast and precise on big programs, typically for malloc, remains an open research 
problem. We are implementing partial solutions that remain correct, but devising ones that are also precise will be challenging.


HTH,


-- 
Boris 
_______________________________________________
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 --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130103/3c679a8c/attachment.html>