--- layout: fc_discuss_archives title: Message 131 from Frama-C-discuss on November 2013 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131129/043496b5/attachment.html>