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

  • Subject: [Frama-c-discuss] Frama-C 19 (Potassium) - beta
  • From: david.buhler at cea.fr (David Bühler)
  • Date: Tue, 14 May 2019 13:33:00 +0200
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.