--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2014 ---
hi David, ?? thanks for investing time to help me out. You and Wolfram are absolutely right. I understand? the importance of loop invariant to provers. I just did not think hard enough about it.? ?? I noticed you moved the s++ into the loop body, so I make little change about the program to ensure correct return value. ?? ---------------------------- ??? const signed char *saved = s;?? // it was "saved = s+1;" before ??? //@ghost int i = 0; ??? //@ghost char *s_init = s; ??? if(NULL==s) ?? { ?????? return (0); ?? } ??? /*@? loop assigns s, i; ???????? loop invariant i>= 0; ???????? loop invariant \forall int j; 0 <= j < i ==> s_init[j] != '\0'; ???????? loop invariant s_init[i] == *s; ???? */ ??? while (*s !=((signed char) '\0')) ??? { ????????? //@ghost i++; ????????? s++; ??? } ??? //@ assert s[i] == '\0'; ??? return (s - saved); ------------------------------------------ ?? It looks to me no more loop invariant is needed for this program.? I tried play around by adding? more assertions,? and adding behaviors clause in contract. But I am still stuck here, that the post condition and assertion can not be proved: [wp] [Z3] Goal typed_szos_strlen_post : Timeout (10s) [wp] [Z3] Goal typed_szos_strlen_assert : Timeout ?? It is likely that I still missed something important in the annotation.? Or,by guessing, could it be automated provers has done their best (so it is time to go to Coq/HOL/... for help)? ?? Unfortunately, I am unable to justify this, eventhough I am thinking pretty hard this time. Any more hints ? cheers, xiaolei ---------------------------------------- Date: Sat, 11 Jan 2014 17:24:09 +0100 From: dmentre at linux-france.org To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] [wp] unproved goals for strlen() function Wolfram is perfectly right, Xiao-lei you need to add loop invariant to *establish* the property you want to prove, i.e. the body of axiom strlen(s). Please find attached an UNFINISHED version of such kind of loop invariants. You'll notice that several things are still unproved. More home work for you. ;-) Best regards, david _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss