--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on July 2012 ---
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 program and the Jessie plugin of Frama-C to deal for 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 lists below. We remind that Why3 and Frama-C must installed before installating Why 2.21. - 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 |