--- layout: fc_discuss_archives title: Message 16 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



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