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] dead code while trying to slice
- Subject: [Frama-c-discuss] dead code while trying to slice
- From: boris at yakobowski.org (Boris Yakobowski)
- Date: Thu, 11 Oct 2012 13:49:31 +0300
- In-reply-to: <20597.59693.848749.582131@cornet.bbn.com>
- References: <20597.59693.848749.582131@cornet.bbn.com>
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 or am I already completely out > of luck due to the recursion flag? > > At a higher level, how do folks go about debugging too much code being > marked as dead when trying to slice? Are there certain messages or > types of messages that I should be particularly looking for or flags > that would be helpful? I can only stress what Patrick said about the importance of having correct dependencies for functions that have no bodies (those that give rise to the warning "No code for function ... default assigns generated"). Except for simple functions, typically those that have no side effect, 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. HTH, -- Boris
- Follow-Ups:
- [Frama-c-discuss] value analysis and system calls
- From: prubel at bbn.com (Paul Rubel)
- [Frama-c-discuss] value analysis and system calls
- 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
- Prev by Date: [Frama-c-discuss] dead code while trying to slice
- Next by Date: [Frama-c-discuss] Approach to compute if-else in Wp and Why
- Previous by thread: [Frama-c-discuss] dead code while trying to slice
- Next by thread: [Frama-c-discuss] value analysis and system calls
- Index(es):