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] Alt-ergo 0.92.1, Frama-C/Why package on Fedora

  • Subject: [Frama-c-discuss] Alt-ergo 0.92.1, Frama-C/Why package on Fedora
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Thu, 07 Oct 2010 09:17:08 +0200
  • In-reply-to: <1986920588.1362137.1286421926531.JavaMail.root@zmbs1.inria.fr>
  • References: <1986920588.1362137.1286421926531.JavaMail.root@zmbs1.inria.fr>
On 10/07/2010 05:25 AM, David A. Wheeler wrote:
> Is alt-ergo 0.92.1 okay/safe to use with the current version of Frama-C + why + Jessie?
>
> Running "why-config" triggers this scary warning:
>   Warning: prover Alt-Ergo version 0.92.1 is not known to be supported, use it at your own risk!
> and the alt-ergo changelog reports "New built-in syntax for the theory of arrays" (!).
>    
Isn't it obvious? Release Alt-Ergo 0.92 appeared recently, while current 
Why version 2.26 was released on May. How could we know in May that 
release 0.92 will come, and how could we know in advance that it would 
work? Same messages can pop up with other external prover too, of course.

This warning will disappear in next Why release. And it is just a warning.

- Claude
> But it *does* seem to work with current frama-c + current why, and alt-ergo 0.92.1
>    
> "Fixes a bug in the arithmetic module" (as noted elsewhere here).
>
> I'm wrapping up packaging why+Frama-C on Fedora (along with Mark Rader), and I'd like to know which version of alt-ergo would be safe to package by default.
>    

There is a known bug with Why versions <= 2.26 and Alt-Ergo 0.91. So I 
do not recommended to package Alt-Ergo 0.91.
Apart from that every combination should be safe.

Finally, notice that  Why 2.27 release, compatible with Alt-Ergo 0.9, 
0.91 and 0.92 is scheduled for december, if it helps.

- Claude







-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |