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:47:03 +0000
  • In-reply-to: <CAEt_dEoZSi6Dgak2Upo4NyaziBRnJmB=LXHTfxaSd0iRni4gKQ@mail.gmail.com>
  • References: <BAY169-W791B99FF16C894E692A16C97E90@phx.gbl> <CAA1cxuhbHXpRvQbopVBNsqNGzVKGAUS1j=xSK-kBr51ggF5nLQ@mail.gmail.com> <CAEt_dEoZSi6Dgak2Upo4NyaziBRnJmB=LXHTfxaSd0iRni4gKQ@mail.gmail.com>
Perhaps I should've been more explicit:

   Here is equivalent to Pre


This is *not* true. the *Here* label refers to the state in which the
annotation is evaluated. eg: when used with *requires*, it refers to the
pre-state, when used in *ensure* it refers to the post-state, when used in
loop invariants it refers to the current iteration.

Omitting the \at clause or using \at( _ , Here) is equivalent, as such: **a
== \at(*a, Here) *will always hold

   By removing the 'Post' label from above annotation, the VCs can be
> generated and proved.


Like I said before, omitting the \at clause is equivalent to \at(*a, Here)

   Pre  is equivalent to Old ?


Yes, \old(*a) == \at(*a, Pre)



2013/11/30 Cristiano Sousa <cristiano.sousa126 at 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
>



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