--- layout: fc_discuss_archives title: Message 25 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



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