--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on January 2014 ---
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>