--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on January 2014 ---
On Sun, Jan 12, 2014 at 06:43:31AM -0500, Xiao-lei Cui wrote: > ?? 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. I am not looking at the details, but in any case, strlen() has a (relatively...) big and complicated \valid precondition (that I am not sure you already wrote down) that is bound to make life hard for you and for automatic provers... Wolfram