--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2013 ---
Hi all, I've encountered a weird behavior when using the WP plugin. In the following function: http://pastebin.com/p0BiC5GP if I include the assertion marked as BUG, de generated POs goes from 55 to 18. Frama-C seems to be ignoring all others. This bug has happened to be before but this is the first time I was actually able to pinpoint the exact cause. On a related note, I'm having a particular hard time proving this particular function. I've had trouble in the past with functions that use unsigned char, the workaround I found was avoid using unsigned char. In this function I cannot do that, since the chars are used to access the matchmap array, and the chars must all be positive to avoid illegal access. -- Regards, Cristiano Sousa -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130621/f500e1c4/attachment.html>