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] Help with proving post-conditions

  • Subject: [Frama-c-discuss] Help with proving post-conditions
  • From: mtorl at hotmail.com (Murat Torlakcik)
  • Date: Wed, 9 Dec 2009 00:15:19 +0000
Hi all,
I'd appreciate some help. I'm unable to prove the following post-conditions although everything else is proved:

    ensures strlen(s) == strlen(\at(s, Old)) + strlen(append);
    ensures \forall integer i; 0 <= i < strlen(\at(s, Old)) ==> s[i] == \at(s[i], Old);
    ensures \forall integer j; strlen(\at(s, Old)) <= j <= strlen(s) ==> s[j] == append[j];


I might have some unnecessary loop invariants there although I didn't add one for old string S's old elements not changing as I assumed loop assigns should cover that. 

Also, I couldn't use more specific assigns[..] clause as it complained about using strlen in there.  I'm using Frama-C Beryllium 2 (with Why 2.21)

 

I hope someone can please give me some pointers.

 



/*@ requires valid_string(s);
    requires valid_string(append);
    requires \valid_range(s, 0, strlen(s) + strlen(append));
    assigns s[..];
    ensures strlen(s) == strlen(\at(s, Old)) + strlen(append);
    ensures \forall integer i; 0 <= i < strlen(\at(s, Old)) ==> s[i] == \at(s[i], Old);
    ensures \forall integer j; strlen(\at(s, Old)) <= j <= strlen(s) ==> s[j] == append[j];
    ensures  \result == s;
 */
char *
strcat(char *s, const char *append)
{
 char *save = s;

 /*@ loop assigns s;
     loop invariant 0 <= (s-save) <= strlen(save);
     loop invariant \valid(s);
     loop invariant \base_addr(s) == \base_addr(save);
     loop invariant \forall integer k; 0 <= k < (s-save) ==> save[k] != 0;
 */
 for (; *s; ++s);


 //@ assert *s == '\0' && s == save + strlen(save);
 //@ assert \valid_range(s, 0, strlen(append));


 //@ ghost char *s_cat = s;
 //@ ghost char *origAppend = append;
 //@ ghost int c = 0;
 //@ ghost int l = strlen(append);
 //@ ghost int l_save = strlen(save);

 

 /*@ loop assigns s, s_cat[..], append;
  loop invariant 0 <= c <= l;
  loop invariant \base_addr(s) == \base_addr(s_cat);
  loop invariant (append-origAppend) == (s - s_cat);
  loop invariant \base_addr(append) == \base_addr(origAppend);
  loop invariant \valid_range(origAppend, 0, l);
  loop invariant \valid_range(s_cat, 0, l);
  loop invariant \forall integer k; 0 <= k < c ==> origAppend[k] != 0;
  loop invariant \forall integer k; 0 <= k < c ==> save[k + l_save] == origAppend[k];
 */
 while ((*s++ = *append++) != '\0'); //@ghost c++;
 return(save);
}

 

Thanks,

Murat.
 		 	   		  
_________________________________________________________________
Windows 7: Find the right PC for you. Learn more.
http://windows.microsoft.com/shop
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091209/76c71e62/attachment.htm