--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on January 2014 ---
On Thu, Jan 23, 2014 at 9:52 AM, Nicky Williams <nicky.williams at cea.fr>wrote: > Of course, static analysis can only detect unreachable code. > To be sure that THERE IS NO unreachable code you need to do path testing, > eg. with the pathcrawler plugin (and to achieve full coverage with no > timeouts). > There are conditions in which the value analysis plug-in is complete as well as sound. In these conditions, it guarantees that code is unreachable and that code is reachable. The following study was made using it under these conditions: http://blog.frama-c.com/index.php?tag/rers2012 . In fact the first part of this very competition was to tell which assertions were reachable and which were unreachable. The conditions under which the value analysis is complete as well as sound will be much easier to express in the next release (to occur at an unspecified date). I may even go as far as documenting them someday after the unspecified date of the new release. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140123/29289472/attachment.html>