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 19 (Potassium) has been released!
- Subject: [Frama-c-discuss] Frama-C 19 (Potassium) has been released!
- From: david.buhler at cea.fr (David Bühler)
- Date: Fri, 21 Jun 2019 16:56:01 +0200
Dear list, It is with utmost pleasure that we celebrate the 100th anniversary of Guy Lux's birth by announcing the release of Frama-C 19.0 (Potassium), which can be used to analyze the schmilblick. Many thanks to all users that have made feedbacks on the betas. A new opam package will be available soon. Please note that opam 2.0 is now mandatory to install new frama-c packages. The Frama-C github repository has been updated: https://github.com/Frama-C/Frama-C-snapshot A complete changelog can be found at: http://frama-c.com/changelog.html Sources and manuals are available at: http://frama-c.com/download.html Main changes with respect to Frama-C 18 (Argon) include: ### Kernel: - new check annotation, similar to assert except that it does not introduce Â additional hypotheses on the program state - new options added to frama-c-script ### GUI: - compatibility with lablgtk3 ### Eva: - New annotation "//@ split exp" to separate the analysis states for each Â possible value of an expression until a "//@ merge exp" annotation. - New option -eva-partition-history to delay the join of the analysis states at Â merging points; useful when a reasoning depends on the path taken to reach a Â control point. - By default, prints a summary at the end of the analysis. - New meta option -eva-precision to globally configure the analysis. - Improved precision on nested loops. ### WP: - new auto-search mode to automatically apply strategies and tactics (see -wp-auto) - extended simplifications on range, bitwise and C-boolean values (_Bool is now Â handled by default) - refactored float model (although it still requires further axiomatisation) ### E-ACSL: - support for user-defined logic functions and predicates without labels - new option -e-acsl-functions that allows the user to specify a white/black list Â of functions in which annotations are monitored, or not. Please don't hesitate to try it out and to provide feedback; reports about possible regressions or improvements on your favorite code are very welcome. Happy verification with Frama-C! For the Frama-C team, Â -- David.
- Prev by Date: [Frama-c-discuss] 3d Call for Papers F-IDE Workshop 2019 (Extended Deadlines)
- Next by Date: [Frama-c-discuss] ACSL by Example (version 19.0.0 for Frama-C 19.0)
- Previous by thread: [Frama-c-discuss] 3d Call for Papers F-IDE Workshop 2019 (Extended Deadlines)
- Next by thread: [Frama-c-discuss] ACSL by Example (version 19.0.0 for Frama-C 19.0)