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



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>