--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Annoucement: release Why 2.28



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)