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] Frama-C: Detecting unreachable code?

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>