Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] [WP] Weird behavior causing many POs not being sent to prover
- Subject: [Frama-c-discuss] [WP] Weird behavior causing many POs not being sent to prover
- From: cristiano.sousa126 at gmail.com (Cristiano Sousa)
- Date: Fri, 21 Jun 2013 14:46:21 +0100
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>