--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why 2.27 released



Why release 2.27 is available on http://why.lri.fr/

This is a bug-fix release compatible with both ocaml 3.12 and earlier 
versions.
The jessie Frama-C plugin is compatible with Frama-C current release Boron.

Here is a excerpt of the changes:

   o [Why] support for Alt-Ergo 0.92.1
   o [Why] fixed compilation with Ocaml 3.12
   o [Why] emacs mode distributed and installed
   o [Why] fixed bug 10851: wrong Coq output for if then else
   o [Why] distinction between computer division and math division
     Fixes Frama-C BTS 0539
   o [Jessie] improved translation of successive assignments on
     the same memory block. As a side effect, translation of
     array initializers from C is much better for provers.
     Fixes Frama-C BTS0377 feature request
   o [Jessie] disabled the experimental support for unions and pointer 
casts,
     since it is too buggy for public release
   o [Jessie] fixed bug with division by zero in expressions evaluated at
     compile-time (fixes Frama-C BTS0473)
   o [Krakatoa] error message when a comment starts with /*(extra space)@
   o [WhyConfig] bug fix when detecting a prover which was removed

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |