--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on June 2018 ---
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>