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