Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] issues with the ACSL Post label

  • Subject: [Frama-c-discuss] issues with the ACSL Post label
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Fri, 29 Nov 2013 00:45:05 -0500
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>