--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on September 2013 ---
Hello, 2013/9/5 BAUDIN Patrick <Patrick.Baudin at cea.fr>: > In addition, it seems that some of yours loop assigns are incorrects, since > the content of the stack is also modified. Yes. For the record, here is attached a fixed version of the program where everything is proved by WP. Best regards, d. -------------- next part -------------- A non-text attachment was scrubbed... Name: q6_stack.c Type: text/x-csrc Size: 1828 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/1952fb2b/attachment.c>