--- layout: fc_discuss_archives title: Message 132 from Frama-C-discuss on November 2013 ---
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