--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2019 ---
Dear Frama-C enthusiasts, We have the pleasure to announce the beta release of Frama-C 19 (Potassium). It is available in the latest branch of Frama-C-snapshot's repository on github: https://github.com/Frama-C/Frama-C-snapshot/tree/latest A link to a tar.gz archive and the manuals are available at https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-19.0-beta-Potassium You can also try it on opam using the following command: opam pin add frama-c "https://github.com/Frama-C/Frama-C-snapshot.git#latest" You are encouraged to try it out and report any potential regression on this list, on https://bts.frama-c.com or on https://github.com/Frama-C/Frama-C-snapshot/issues. Barring any critical issue, the final Frama-C 19 release is scheduled for late May. Main changes 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. For the Frama-C team,  -- David.