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

  • Subject: [Frama-c-discuss] [wp] unproved goals for strlen() function
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Thu, 9 Jan 2014 05:11:31 -0500
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>