--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C Carbon 20110201



Dear Frama-C users,

we are happy to announce the release of Frama-C Carbon 20110201. It
does not include plugin WP; WP will shortly be
released separately. Likewise, a new version of Why
compatible with Carbon should appear soon, as well as the
excellent binary releases you have come to expect for stable versions.

Main changes since Carbon 20101202 beta2 include (see
http://frama-c.com/Changelog.html#Carbon-20110201 for the full
Changelog)
- display more precise state after statement in the GUI
- Gui options start with -gui and not -GUI
- assigns x; in the specification of function f is now an error when x
  is a formal of f (assigns *x; is still valid of course)
- improved precision of value analysis on bitwise operators
- improved interpretation of ACSL annotations in value analysis
- value analysis generates smaller initial state when -lib-entry is set
- better performance on platforms with dynamic loading
- better handling of exceptions in exit routines of Frama-C
- better performance of value analysis plugin
- fix 100% cpu load in GUI while external commands are launched
- bugs fixed: 313, 635, 637, 638, 645, 647, 660, 666, 668, 673, 677

Changes only visible to developers include:
- refactoring of the AST representation of assigns and from
- Property.identified_property is now a private type
- Remove of the API Messages.{enable_collect,disable_echo,depend}
- New functions Kernel_function.find_syntactic_callsites and
  Plugin.add_aliases

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98