--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on January 2014 ---
Hi Dr Kahl, ??? I did removed some pre-conditions. Thanks for the reminder. ??? Now I added them to the contract: /*@ predicate valid_string{L}(signed char *s) = ? @?? 0 <= strlen(s) && \valid(s+(0..strlen(s))); ? @ ? @ predicate valid_string_or_null{L}(signed char *s) = ? @?? s == \null || valid_string(s); ? @*/ /*@ ??? requires valid_string_or_null(s); ??? requires s==NULL || s == EOS || *(s+strlen(s))==EOS; ??? assigns \result; ??? ensures \result == strlen(s); @*/ ?? ?? However, Z3 and CVC3 still struggled with the post-condition and the last assertion: [wp] [Z3] Goal typed_szos_strlen_post : Timeout (Qed:4ms) (10s) [wp] [Z3] Goal typed_szos_strlen_assert : Timeout (10s) ? cheers xiaolei > 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 > > > _______________________________________________ > 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