Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Release 2.32 of Why/Krakatoa/Jessie
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 27 Mar 2013 09:29:40 +0100
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                    |