--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2013 ---
We are pleased to announce that a new release 2.32 of Why is available, that includes updated versions of the Krakatoa front-end for Java programs and the Jessie plug-in of Frama-C. The main purpose of this release is to provide new versions of Krakatoa and Jessie that are compatible with both Frama-C Oxygen and the just-released Why3 0.81. The main changes are as follows. o [Jessie/Why3ML output] Compatible with release 0.81 of Why3 o [Jessie/Frama-C plugin] support for "allocates" clause in contracts o [Jessie/Frama-C plugin] support for built-in construct \fresh o [Jessie/Frama-C plugin] support for ACSL model fields o [Jessie memory model] added an axiom for sub_pointer o [Jessie memory model] fixed bug in Why3 version (free_parameter) see Frama-C BTS 1251 o [Jessie/Frama-C plugin] added new -jessie-atp=why3replay to replay Why3 proofs o [Jessie] fixed Frama-C BTS 1265 Here are also the main changes of Why3 0.81 that have an impact on Krakatoa and Jessie users o [stdlib] fixed inconsistency in map.MapPermut theory o [prover] fixed Coq 8.4 support for theory real.Trigonometry o [prover] support for Gappa up to 0.16.6 o [prover] support for Z3 4.2, 4.3.* o [prover] support for Alt-Ergo 0.95.1 o [prover] support for CVC4 o [prover] support for PVS 6 o [prover] experimental support for mathematica o [prover] experimental support for MathSAT5 Best regards, - Claude -- 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 |