--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on September 2015 ---
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