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