--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Release 2.32 of Why/Krakatoa/Jessie



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                    |