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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Fri, 19 Apr 2013 14:29:06 +0200
  • In-reply-to: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com>
  • References: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com>
Hello,

2013/4/19 Cristiano Sousa <cristiano.sousa126 at gmail.com>:
> I'm very excited in finally having a new version of frama-c.

Well, many thanks for your quick feedback ;-)

>
> Installation went smooth, and the first thing I did was checking POs of the
> project I'm currently am working on.
>
> The new memory model seems powerfull, sadly I cannot prove a simple function
> using alt-ergo (previously i could), and also cannot use why3 as it returns
> an error related to unbound variables:
>

I suppose you're speaking about the WP plugin. Which version of
alt-ergo and Why3 are you using? In particular, Frama-C Oxygen is only
compatible with alt-ergo <= 0.94, while if I'm not mistaken Frama-C
Fluorine works with alt-ergo>=0.95 (there has been an incompatible
change in Alt-ergo's input syntax between the two versions).

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile