Log Message:
Update to Frama-C Nitrogen release 2011-10-01
See full list of changes at http://frama-c.com/Changelog.html#Nitrogen-20111001

Nitrogen Release [20111001]

Frama-C General

New Features

  * [Cil]   Enumerated constants are kept in the AST.
  * [Cil]   Implement precise dataflow on switch constructs. As side effect, \ 
improve precision of value analysis.
  * [Cil]   Fixed #720 (incorrect simplification of switch).
  * [Cil]   Support for &"constant_string" in parser.
  * [Cil]   Normalization of lval: T+1 ==> &T[1] when T is in fact an \ 
array (implies *(T+1) ==> T[1])
  * [Cil]   Pretty-printing lval and term_lval the same way
  * [Cil]   Cache results of offsets computations.
  * [Cil]   Add support for GCC specific cast from field of union to union
  * [Kernel]   Exit status on unknown error is now 125. 127 and 126 are reserved \ 
for the shell by POSIX.
  * [Kernel]   Better error message when plug-in crashes on loading (bts #737).
  * [Kernel]   Big integers can now be displayed using hexadecimal notation.
  * [Kernel]   \at(p,Old) is pretty-printed as \old(p).
  * [Kernel]   Some messages may be printed several time for the same line if \ 
they refer to different columns.
  * [Kernel]   Better handling of comments with -keep-comments and new API. See \ 
Cabshelper.Comments and Globals.get_comments_*
  * [Kernel]   Better pretty printing of lists of any elements
  * [Kernel]   Current pragmas no longer give rise to code annotations (as they \ 
do not contain anything that can be proven).
  * [Kernel]   Improve space complexity of function stmt_can_reach.
  * [Kernel]   New kind of command-line parameter, for commands that do heavy \ 
output. Used for Value, Pdg and Metrics.
  * [Logic]   Added support for bitwise operators --> and <--> into \ 
ACSL formula.

Carbon Release [20110201]

Frama-C General

New Features

  * [Configure]   Frama-C does not require Apron anymore (Why does for Jessie). \ 
Thus fix bug #647.
  * [Kernel]   Improve performance on platform with dynami.c loading. Mainly \ 
impact value analysis (for developers: improve
    efficiency of Dynamic.get).
  * [Kernel]   Handle errors better when they occur when exiting Frama-C. Slight \ 
semantic changes for exit code: - old code 5 is now
    127; - code 5 is now: error raised when exiting Frama-C normally; - code 6: \ 
error raised when exiting Frama-C abnormally.
  * [Logic]   Fix priority bug in parser.
  * [Logic]   Mentioning a formal on the left-hand side of an assigns clause is \ 
now an error when type-checking logic annotations.
  * [Makefile]   Fixed bug #638. By default, warnings are no more errors when \ 
compiling a public Frama-C distribution and plug-ins.
    SVN versions of Frama-C are still compiled with "-warn-error A".

Carbon Release [20101201]

Frama-C General

New Features

  * [Cil]   Be less agressive during inline function merge. Alpha equivalent \ 
function are now kept separate.
  * [Cil]   Clean up local variables handling and pretty-printing modified \ 
pBlock method interface (unified pBlock and pInnerBlock)
  * [Cil]   Cil normalization takes care of abrupt clauses
  * [Configure]   Better detection of native dynlink support.
  * [Kernel]   Feature #484 about requires into named behaviors
  * [Kernel]   Fixed bug #548: limit.h now syntactically correct. Architectures \ 
other than x86_32 still unsupported.

Boron Release [20100401]

Frama-C General

New Features

  * [Cil]   Extend logic pretty printer to handle all specific clauses
  * [Configure]   Dynamic plug-ins are now statically linked by default whenever \ 
native dynlink is not usable (bts #301).
  * [Configure]   Compiling the GUI now requires LablGnomeCanvas.
  * [Kernel]   Add status for all clauses
  * [Kernel]   Clarification of the multiple accesses warning. Becomes \ 
"undefined multiple accesses in expression".
  * [Kernel]   Better error messages when a dynamic plug-in cannot be loaded.
  * [Kernel]   Better -*-help.
  * [Kernel]   New option -no-dynlink in order to prevent loading of dynamic \ 
plug-ins.
  * [Kernel]   The journal is generated only if the GUI is crashing, or if the \ 
option -journal-enable is explicitely set (fixed issue
    #330).
  * [Kernel]   Backtrace when Frama-C is crashing (only if Frama-C is compiled \ 
with caml >= 3.11.0)
  * [Kernel]   New option "-plugin-h" as an alias for option \ 
"-plugin-help"
  * [Kernel]   Preliminary standard C library in $FRAMAC_SHARE/libc
  * [Logic]   Better error message when using = in annotations
  * [Logic]   ordering of clauses in contracts
  * [Logic]   If a C typedef integer, real or boolean exists, it takes \ 
precedence over corresponding logic type. The logic type
    remains accessible through its utf-8 denomination.
  * [Logic]   Support for type abbreviation in logic
  * [Logic]   Support for "reads \nothing"
  * [Logic]   Adding "\pi" as built-in symbol

Beryllium Release [20090902]

Frama-C General

New Features

  * [Configure]   Detection of dot if required.
  * [Journal]   Better handling of exceptions.
  * [Kernel]   Slightly less false alarms with -warn-unspecified-order
  * [Makefile]   Why is no longer a compilation dependency. It is required only \ 
at runtime for the experimental WP plugin.
  * [Makefile]   Now possible to build custom binaries for plug-ins. Roughly \ 
these binaries are frama-c[.byte] + the plug-in
    statically-linked. The goal is called "static" in the plug-in's \ 
makefile.