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] Specification Examples

  • Subject: [Frama-c-discuss] Specification Examples
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Thu Oct 9 15:44:10 2008
Hello,

I'm exercising with the jessie-tool learn the usage of the ACSL-Language.
I have two examples. My Problem is with the second one.

#1: works fine, i get green bullets
/*@ 
 requires 0 < n;  
 requires \valid_range(a, 0, n-1);
 ensures  \forall int i; 0 <= i < n ==> a[i] == 0;
*/
void array_zero(int* a, int n){ 
 /*@ loop invariant 0 <= i <= n && \forall int k; 0 <= k < i ==> a[k] == 0; 
 */
 for(int i = 0;i< n;i++){
  a[i]=0;
 } 
}

#2: in the second example the preservation of the loop invariant wont work



/*@ 
 requires 0 < n;  
 requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
 ensures  \forall int k; 0 <= k < n ==> a[k] == b[k];
*/
void array_cpy(int* a, int n, int* b){ 
 /*@ loop invariant 0 <= i <= n && \forall int m; 0 <= m < i  ==> a[m] == b[m];
 */
 for(int i = 0;i< n;i++){    
  a[i]=b[i];    
 } 
}


What am I missing, to get the examples running?

Christoph


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081009/7620ab3b/attachment.htm