--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issues with WP on program doing simplepointer arithmetic



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>