--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Porting some simple example from Jessie to WP



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>