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] Why 2.27 released

  • Subject: [Frama-c-discuss] Why 2.27 released
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Thu, 14 Oct 2010 10:44:52 +0200
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                    |