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>