--- layout: fc_discuss_archives title: Message 15 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,
   Thanks. You are right, the "loop assigns" cluase is wrong. 
  
/*@
  loop assigns s;
 */
 while (*s++ !=((signed char) '\0'))
 {
    ;
 }
    This will discharge the following proof obligation:
[wp] [Z3] Goal typed_strlen_loop_assign_part3.  
  
    But the post condition is still left unproved.  The spec seems to be correct? and  the automatic prover can not prove it due to complexity. I want to try Coq this time.

xiaolei
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140111/08d69e6b/attachment.html>