--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on September 2013 ---
Hello Dillon and Lo?c, 2013/9/4 Lo?c Correnson <loic.correnson at cea.fr>: > 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 ! OK, thank you for the explanations. > Somebody else reported a simiar problem recently, but I can not figure out > what is the origin. Should I attach my example to this bug report? If yes, what is its identifier? > As reported by Dillon, rephrasing the code can help. We are investigating > the problem ! I'll use Dillon work-around for now. I'll try to keep the -print normalization in mind for my production code. Thanks for the quick feedback! david