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] WP RTE mem_access condition is Unknown

  • Subject: [Frama-c-discuss] WP RTE mem_access condition is Unknown
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 23 May 2014 22:33:21 +0200
  • In-reply-to: <1400876442.8745.6.camel@one>
  • References: <1400876442.8745.6.camel@one>
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>