--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on June 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C 17 (Chlorine) has been released!



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>