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

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