--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on January 2014 ---
[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