--- layout: default date: 21-06-2019 title: Release of Frama-C 19.0 (Potassium) --- Frama-C 19.0 (Potassium) is out. Download it [here](/fc-versions/potassium.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. A complete changelog can be found [here](/html/changelog.html#Potassium-19.0).