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: prubel at bbn.com (Paul Rubel)
- Date: Tue, 16 Oct 2012 14:58:43 -0400
- In-reply-to: <CABbVA-CD1iNrrWFcozRyARucyLo78zhZOFz6b-wS6j9fWXdGTg@mail.gmail.com>
- References: <20597.59693.848749.582131@cornet.bbn.com> <CABbVA-CD1iNrrWFcozRyARucyLo78zhZOFz6b-wS6j9fWXdGTg@mail.gmail.com>
Thanks for your previous help Boris and Patrick, Boris Yakobowski writes: > Hello, > > On Thu, Oct 11, 2012 at 12:31 AM, Paul Rubel <prubel at bbn.com> wrote: > > Do I need to address all the assertions, which are marked as warnings, > > before I can expect a reasonable slice? > I can only stress what Patrick said about the importance of having > correct dependencies for functions that have no bodies > you should review carefully the ACSL 'assigns' clause > that is guessed for each function, and write a correct one yourself if > needed. > If the missing functions are those of the standard C library, > try to parse your application with the file share/libc/fc_runtime.c or > share/libc/posix_fc_runtime.c (with the appropriate -I directives). > With luck, you should obtain much better results with little effort. I've spent some time trying to sort out all the default assigns that were being generated during value analysis. Some of the calls I was trying to figure out were clearly foreseen by the documentation writes, such as memcpy and I was able to fix those calls. Others were more complicated and I tried to add -cpp-extra-args="-I`frama-c -print-path`/libc" to my frama-c invocation. This lead to compile errors as more headers were pulled in, such as /usr/include/bits/utmp.h. Is there a particular architecture/distribution/something else that works well with the framc-c/libc headers? 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? Thanks again for the help, Paul
- References:
- [Frama-c-discuss] dead code while trying to slice
- From: prubel at bbn.com (Paul Rubel)
- [Frama-c-discuss] dead code while trying to slice
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] dead code while trying to slice
- Prev by Date: [Frama-c-discuss] Unsupported extension : Length of array size is zero.
- Next by Date: [Frama-c-discuss] Unsupported extension : Length of array size is zero.
- Previous by thread: [Frama-c-discuss] dead code while trying to slice
- Next by thread: [Frama-c-discuss] Approach to compute if-else in Wp and Why
- Index(es):