--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on July 2012 ---
Sorry, I sent the mail a bit too early, without reading what I wrote... let me fix the numerous typos: A new release of Why (version 2.31) is available from the site http://why.lri.fr This release provides a new version of the Krakatoa tool for Java programs and the Jessie plugin of Frama-C to deal with C programs. (See http://krakatoa.lri.fr/) The main purpose of this new release is to be compatible with the new release 0.73 of the Why3 environment (intermediate language, VC generator, multi-provers back-end, proof sessions tools). There are a few new features listed below. We remind that Why3 and Frama-C must be installed before installing Why 2.31. - Claude o [Jessie/Why3ML output] Compatible with release 0.73 of Why3 o [Jessie/Why3ML output] Fixed bug with translation of the if expression, which expect a prop in Why3, instead of a term o [Jessie and Krakatoa] support for "allocates" clause in contracts o [Jessie and Krakatoa] support for built-in construct \fresh o [Jessie/Why3ML output] avoid Why3 keywords, fixed Frama-C BTS 1004 -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |