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] [wp] unproved goals for strlen() function

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