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



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>