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



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>