Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] issues with the ACSL Post label
  • From: cristiano.sousa126 at gmail.com (Cristiano Sousa)
  • Date: Sat, 30 Nov 2013 14:30:45 +0000
  • In-reply-to: <CAA1cxuhbHXpRvQbopVBNsqNGzVKGAUS1j=xSK-kBr51ggF5nLQ@mail.gmail.com>
  • References: <BAY169-W791B99FF16C894E692A16C97E90@phx.gbl> <CAA1cxuhbHXpRvQbopVBNsqNGzVKGAUS1j=xSK-kBr51ggF5nLQ@mail.gmail.com>
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>