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] New Frama-C version: Fluorine

  • Subject: [Frama-c-discuss] New Frama-C version: Fluorine
  • From: cristiano.sousa126 at gmail.com (Cristiano Sousa)
  • Date: Sat, 4 May 2013 18:07:16 +0100
  • In-reply-to: <51791A07.40706@free.fr>
  • References: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com> <51791A07.40706@free.fr>
Hi,

I'm having a odd problem with proving a simple contract with the WP plugin.
I'm forced to insert the assertions HELPER and HELPER2 in order to
discharge all POs, when in the Oxygen release I didn't need this kind of
assertions. Without HELPER, BOUND cannot be proved and without HELPER2 the
post condition cannot be proved. Note: the rest of the assertions were
inserted to help me pinpoint the problem.

http://pastebin.com/p5AdPN2n

Also, in the previous release of frama-c there was a problem with cvc3
processes not being killed. This problem now happens more ofter but i'm
guessing this is a problem related to why and not frama-c.

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130504/d5275649/attachment.html>