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] value analysis and system calls

  • Subject: [Frama-c-discuss] value analysis and system calls
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Wed, 2 Jan 2013 20:27:52 +0100
  • In-reply-to: <20605.44643.989750.208972@cornet.bbn.com>
  • References: <20597.59693.848749.582131@cornet.bbn.com> <CABbVA-CD1iNrrWFcozRyARucyLo78zhZOFz6b-wS6j9fWXdGTg@mail.gmail.com> <20605.44643.989750.208972@cornet.bbn.com>
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130102/dfa6a2a0/attachment.html>