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