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 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