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

  • Subject: [Frama-c-discuss] Frama-C 17 (Chlorine) - beta
  • From: Thibaud.ANTIGNAC at cea.fr (ANTIGNAC Thibaud)
  • Date: Tue, 24 Apr 2018 08:47:35 +0000
Dear Frama-C enthusiasts,

 

We have the pleasure to announce the beta release of the next version of Frama-C, 17 (Chlorine).

 

It is available in the release-candidates branch of Frama-C-snapshot's repository on github: https://github.com/Frama-C/Frama-C-snapshot/tree/release-candidates.

You can try it on opam using the following command: opam pin add frama-c "https://github.com/Frama-C/Frama-C-snapshot.git#release-candidates";

A link to a tar.gz archive and the manuals is available at https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-Chlorine-20180501-beta.

You are encouraged to try it out and report any potential regression on this list or on this list, https://bts.frama-c.com, or on https://github.com/Frama-C/Frama-C-snapshot/issues.

 

Barring any critical issue, final Frama-C 17 release is scheduled for late May.

 

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

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/20180424/85883b9c/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5133 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180424/85883b9c/attachment-0001.bin>