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

Dear Frama-C enthusiasts,

We have released a second beta for Frama-C 19 (Potassium).
We believe we have fixed in this new version all the regressions that 
were reported to us.

As for the previous one, the new beta 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 tar.gz archive and the manuals are available at 
https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-19.0-beta2-Potassium
You can also install it on opam using the following command: opam pin 
add frama-c "https://github.com/Frama-C/Frama-C-snapshot.git#latest";

You are still encouraged to try it out and report any potential 
regressions on this list,
on https://bts.frama-c.com or on 
https://github.com/Frama-C/Frama-C-snapshot/issues.

Barring any new critical issue, the final Frama-C 19 release is 
scheduled for mid-June.

For the Frama-C team,
  --
David.

Le 14/05/2019 à 13:33, David Bühler a écrit :
> 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.
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss