--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP RTE mem_access condition is Unknown



On Fri, May 23, 2014 at 10:20 PM, Mansour Moufid <mansourmoufid at gmail.com>wrote:

>
> But this program does not produce the same result:
>
>     int b(int x)
>     {
>         return (x > 0);
>     }
>     /*@ requires \valid(x);
>      */
>     void a(int *x, const int y)
>     {
>         if (b(y) != 0) {
>             *x = y;
>         }
>         return;
>     }
>
>
You should provide function b() with a contract, otherwise, how can the WP
plug-in know what it does? The assigns clause would be the important part
of that contract, since it would tell that the x being dereferenced is the
same as the x that the precondition says is valid.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140523/ab42afbb/attachment.html>