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 Sat, Jan 25, 2014 at 8:43 PM, Dharmalingam Ganesan <
dganesan at fc-md.umd.edu> wrote:

> Thanks, but replacing the ensures by \false still proves correct.
>

Which should tell you something.


> The code is incorrect (comparing an unsigned int to < 0) but  WP is not
> pointing me this error.
>

The WP plug-in is designed for proving the functional correctness of a
piece of C code: if such-and-such conditions are true of the state in which
the code is invoked, then so-and-so conditions hold for the resulting state
after the target code has been executed.

In much the same way that all elements of the empty set are pink, for all
memory sets satisfying i<0 that you can invoke your function in, the
resulting state satisfies \result == -1 (and also satisfies \false).

If you consider that comparing an expression of unsigned type to zero is
?incorrect?, and that is only *your* definition (the standard makes it
clear what the result of this comparison is, and it's not undefined. In
fact it is one of the better-defined operations), you could write your own
plug-in that detects such comparisons. It is not the role of either
Frama-C's value analysis or WP to detect such comparisons.

Note that I am not saying that writing a Frama-C plug-in is easy, that the
APIs are documented or that you are entitled to be helped for free in this
endeavor. I am only saying that if your goal is to detect strange
comparisons, the existing Value and WP plug-ins were not designed to be
solutions to your problem.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140125/e7301a40/attachment.html>