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] Frama-C 17 (Chlorine) has been released!

  • Subject: [Frama-c-discuss] Frama-C 17 (Chlorine) has been released!
  • From: Thibaud.ANTIGNAC at cea.fr (ANTIGNAC Thibaud)
  • Date: Fri, 1 Jun 2018 07:22:48 +0000
Dear Frama-C enthusiasts,

Today, we honor the memory of Évariste Galois by releasing Frama-C 17 (Chlorine) from Papeete, French Polynesia.

Main changes with respect to Frama-C 16 - Sulfur include:

  *   KERNEL
     *   Added option -inline-calls for syntactic inlining
     *   Introduced warning categories: possibility of disabling some warnings, converting warnings into errors and vice-versa, and more detailed warning messages
     *   Added support for CERT EXP46-C
     *   Extra-type checking verifications (e.g. in function pointer compatibility and lvalues assignments)
     *   Added support for JSON compilation databases, a.k.a. compile_commands.json (optional: requires package 'yojson')

  *   EVA
     *   Added support for infinite floats and NaN (via option -warn-special-float)
     *   Added a new panel "Red alarms" in the GUI that shows all properties for which a red status has been emitted for some states during the analysis. They may not be completely invalid, but should often be investigated first
     *   Evaluate the preconditions of the functions for which a builtin is used; builtins do not emit alarms anymore
     *   The subdivision of evaluations (through the option -val-subdivide-non-linear) can subdivide the values of several lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y)
     *   Various improvements in the equality domain which is now inter-procedural (equalities can be propagated through function calls)

  *   WP
     *   Support for ACSL math builtins (\sqrt, \exp, \log, etc.) and _Bool type
     *   Improved Qed simplifications in many domains
     *   Upgrade reference versions for provers (Alt-Ergo 2.0.0, Coq 8.7.1 and Why-3 0.88.3)
     *   New and/or enhanced tactics available from the graphical user-interface
     *   Searching for strategies from the command line

  *   E-ACSL
     *   New option -e-acsl-validate-format-strings to detect format string vulnerabilities in printf-like functions

The Frama-C Github repository has been updated: https://github.com/Frama-C/Frama-C-snapshot
The new opam package will be available soon.
As usual, the complete Changelog can be found at: http://frama-c.com/changelog.html
Sources and manuals are available at: http://frama-c.com/download.html

Have fun with Frama-C!

For the Frama-C team,
--
  Thibaud Antignac
  CEA List
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180601/b2fbfa3e/attachment.html>