--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2010 ---
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)