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



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