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] New release 2.24 of Why

  • Subject: [Frama-c-discuss] New release 2.24 of Why
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Mon, 19 Apr 2010 14:02:51 +0200
A new release, version 2.24, of Why is available for download, from 
http://why.lri.fr/

This version provides a new version of the Jessie Frama-C plugin, 
compatible with Frama-C Boron 20100412

Here is a list of the main important changes, which concern the Frama-C 
plugin

* The "defensive" model for floating-point computations is now the 
default. The former model,
  which interprets floating-point computations into mathematical real 
numbers without rounding,
  can be activated using
    #pragma JessieFloatModel(math)

  This impacts all code using "float" or "double" variables.

  More information about this model can be found in the following 
article, to appear in the
  proceedings of the IJCAR 2010 conference :

@inproceedings{ayad10ijcar <http://proval.lri.fr/publications/2010-conference.html#ayad10ijcar>,
  author = {Ali Ayad and Claude March\'e},
  title = {Multi-Prover Verification of Floating-Point Programs},
  url = {http://www.lri.fr/~marche/ayad10ijcar.pdf <http://www.lri.fr/%7Emarche/ayad10ijcar.pdf>},
  booktitle = {Fifth International Joint Conference on Automated Reasoning},
  year = 2010,
  editor = {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  address = {Edinburgh, Scotland},
  month = jul,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer}
}

  A gallery of verified programs using this model can be found on the Hisseo project Web page:
  http://hisseo.saclay.inria.fr/gallery.html



* The pragma TerminationPolicy, to allow the user to prevent generation of VCs for termination, 
  is now available
  

* logic functions do not accept struct or union as parameters. You are 
enforced to
   add an indirection use a pointer. See 
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001848.html

* many bug-fixes, including several bug fixes regarding statement 
contracts and named behavior.
  See the file CHANGES for the details

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