--- layout: fc_discuss_archives title: Message 28 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



Sorry, I sent the mail a bit too early, without reading what I wrote... 
let me fix the numerous typos:

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
programs and the Jessie plugin of Frama-C to deal with 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 listed below.

We remind that Why3 and Frama-C must be installed before installing Why
2.31.

- 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                    |