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] Annoucement: release Why 2.28

  • Subject: [Frama-c-discuss] Annoucement: release Why 2.28
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Sat, 18 Dec 2010 09:51:54 +0100
Why release 2.28 is now available on http://why.lri.fr/

This release provides a new version of the Jessie plugin which is now 
compatible with Frama-C release "Carbon". Note: it is *not* compatible
with earlier versions of Frama-C.

It also provides a few changes with Why 2.27: support for more provers 
or more recent versions of provers, and a few bug fixes. A special 
effort was made to replace uninformative messages (like "assertion 
failure") by more informative ones. See also the new section "trouble 
shooting" at the end of the Jessie documentation (in the Frama-C 
distribution, and hopefully soon on the Frama-C web page).

There is also a special new feature, which will be announced in a few days.

Below is an excerpt of the changes, see file CHANGES for more details.

Hoping this is useful,

Merry Christmas to all!

- Claude




   o [Why] support for Coq 8.3
   o [Why] support for Alt-Ergo 0.92.2
   o [Coq output] removed dependencies on Float and Gappa libraries,
     added dependency on Flocq library
   o [Jessie] emit a warning when generating a dummy variant for
     recursive functions and loops (Frama-C bug 512)
   o [Jessie] preliminary support for \at in region computation
   o [Why] added --smtlib-v1 option (default smtlib format is v2.0)
   o [Why] added support for verit prover
   o [Why] improved support for integer division (better triggers)