--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on December 2009 ---
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