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.