--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2014 ---
Hi all, ??? I am using Frama-c-fluorine and wp-0.7, to prove string functions from standard C library.? The ACSL spec is taken from some header files shipped with why platform. The code and spec is attached. ??? I tried 3 provers: alt-ergo , cvc3, and z3, but all of them failed on the last 2 goal: $ frama-c -wp -wp-prover z3 str_len.c [kernel] preprocessing with "gcc -C -E -I.? str_len.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 10 goals scheduled [wp] [Qed] Goal typed_strlen_loop_assign_part1 : Valid [wp] [Qed] Goal typed_strlen_loop_assign_part2 : Valid [wp] [Qed] Goal typed_strlen_assign_part1 : Valid [wp] [Qed] Goal typed_strlen_assign_part2 : Valid [wp] [Qed] Goal typed_strlen_assign_part3 : Valid [wp] [Qed] Goal typed_strlen_assign_part4 : Valid [wp] [Qed] Goal typed_strlen_assign_part5 : Valid [wp] [Qed] Goal typed_strlen_assign_part6 : Valid [wp] [Z3] Goal typed_strlen_loop_assign_part3 : Unknown [wp] [Z3] Goal typed_strlen_post : Timeout (Qed:4ms) (10s) ?? Perhaps I mis-annotate somewhere. Any ideas to fully prove this function? ?? many thanks! xiao-lei -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: str_len.c URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140109/931818e4/attachment.c>