--- layout: fc_discuss_archives title: Message 81 from Frama-C-discuss on January 2014 ---
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>