--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C 19 (Potassium) - beta



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.