--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on August 2015 ---
On Thu, Aug 27, 2015 at 6:40 PM, Tim Newsham <tim.newsham at gmail.com> wrote: > proves everything except the assertion >> /*@ assert \initialized(buf + (32..40)); */ >> >> This is good because >> - I'm not convinced it is a true assertion >> - /*@ assert \initialized(buf + (32..39)); */ is sufficient, and can be >> proven >> > > hrmm.. indeed.. this scares me because my previous analysis > didnt catch this! > I looked into this and to my surprise frama-c's textual output doesnt include a warning for this unverified assertion, but when I loaded it up in the gui, it was clearly marked as yellow. I had previously assumed that no warnings in the output meant that everything was good. Is there a way to force warnings in the output for all unverified assertions? Also thank you for the other email about the fopen issue. I don't > recall fopen reporting dead code in my model of fopen but I'll > revisit the issue as I digest the ideas in your email further. > I verified that the sodium version isnt reporting any dead code in my fopen model. Perhaps it's unique to the newest version? At any rate, I'm planning on retrying my tests in the latest version soon. Once again, thank you for your feedback.. It's been very helpful. -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150827/912d2d60/attachment-0001.html>