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