--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on September 2015 ---
Hi, For teaching, I am trying to port some examples I have to WP, the following example could be proved by jessie, but it doesn't work with WP. Can I have a hint ? /*@ requires \valid(x)&&-10<*x<10; requires \valid(y)&&-10<*y<10; assigns *x; assigns *y; ensures *x == \old(*y); ensures *y == \old(*x); */ void echange(int *x, int *y) { *x=*x+*y; *y=*x-*y; *x=*x-*y; return; } Regards, Julien Narboux -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150921/4e7606de/attachment.html>