--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New release of Why and the Jessie plugin of Frama-C



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                    |