--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on September 2013 ---
Hi, In addition, it seems that some of yours loop assigns are incorrects, since the content of the stack is also modified. Patrick. 04/09/2013 16:21, Lo?c Correnson wrote: > Hi, > > It seems that, actually, many proof obligations are missing. > The simple invariant over variable i is easily discharged on simple > goals, but the proof obligation for preservation is missing in your > case. There is a dangling node in the internal CFG generated by WP for > your code, but don't know why ! > > Somebody else reported a simiar problem recently, but I can not figure > out what is the origin. > As reported by Dillon, rephrasing the code can help. We are > investigating the problem ! > > L. -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/1e67b1ed/attachment.html>