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: dwheeler at dwheeler.com (David A. Wheeler)
  • Date: Wed, 06 Oct 2010 23:25:15 -0400 (EDT)
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" (!).
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.

Thanks.

--- David A. Wheeler