--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help with proving post-conditions



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