--- layout: fc_discuss_archives title: Message 133 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] issues with the ACSL Post label



You could try Here instead of Post.

ensures (\at(*x, Here)== \at(*y,Pre)) && (\at(*y, Here) == \at(*x,Pre)) ;


or just simply:

ensures ( *x == \at(*y,Pre)) && ( *y == \at(*x,Pre)) ;


or even:

ensures ( *x == \old(*y) && ( *y == \old(*x)) ;



2013/11/30 David Yang <abiao.yang at gmail.com>

> ensures (\at(*x, Post)== \at(*y,Pre)) && (\at(*y, Post) == \at(*x,Pre)) ;
>
> I remember the keyword of Post and Pre are for loop invariant/
> variant. But I am not very sure, I recommend you to check this in the
> ACSL document.
>
> On 29 November 2013 05:45, Xiao-lei Cui <x_cui at hotmail.com> wrote:
> >
> > Hi all,
> >    When I document code with the ACSL 'Post' label, in the 'ensures'
> clause,
> > Jessie raised some typing error. I tried again in a simple program that
> > swaps two integers:
> >
> > /*@
> >   requires \valid(x);
> >   requires \valid(y);
> >   assigns *x;
> >   assigns *y;
> >   ensures (\at(*x, Post)== \at(*y,Pre)) && (\at(*y, Post) ==
> \at(*x,Pre)) ;
> > */
> >
> > void swap(int* x, int *y){
> >   int temp;
> >   temp = *x;
> >   *x = *y;
> >   *y = temp;
> > }
> >    I got jessie error message:
> > File "swap.jc", line 50, characters 26-51: typing error: label `Post' not
> > found
> > [jessie] user error: Jessie subprocess failed:   jessie  -why3ml  -v
> -locs
> > swap.cloc swap.jc
> >
> >    By removing the 'Post' label from above annotation, the VCs can be
> > generated and proved. I read the ACSL manual, but still cannot figure out
> > why jessie failed. Moreover, the interpretation for Pre, Here, Post, and
> > Old, confuses me sometimes. In a function's contract annotation(like
> > annotation for swap()), is it true that
> >    Here is equivalent to Pre
> >    Pre  is equivalent to Old ?
> >    Could someone help me clarify this?  :) Thanks.
> >
> > cheers
> > xiao-lei
> >
> >
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Cumprimentos,
Cristiano Sousa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131130/dda637d1/attachment.html>