--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on September 2015 ---
Thanks a lot for the quick reply. Regards, Julien 2015-09-21 10:00 GMT+02:00 Virgile Prevosto <virgile.prevosto at m4x.org>: > Hello, > > 2015-09-21 9:49 GMT+02:00 Julien Narboux <jnarboux at narboux.fr>: > > 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; > > } > > Contrarily to Jessie, WP does not assume by default that your pointers > arguments are separated. You have to either provide an explicit > pre-condition (requires \separated(x,y);) or use the Typed+ref memory > model (on the GUI, just click on the Model button in the WP panel on > the left and tick the Ref box, on command line use -wp-model Typed+ref > option). +ref considers more or less that in the initial state of the > function there are no aliases, see WP manual for more information. > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150921/4327c992/attachment.html>