-! Kernel [2012/09/17] Remove useless negative options -no-help,
-no-version, -no-print-share-path, -no-print-lib-path and
-no-print-plugin-path.
o!* Cil [2012/09/12] Split constants of logic and C (fixes bts #745).
o! Cil [2012/09/12] Remove type Cil_type.typsig. Use the functions in
Cil_datatype.Typ and Cil_datatype.Logic_typ to compare types.
o! Kernel [2012/09/03] Remove obsolete constructors Cabs.TRANSFORMER and
Cabs.EXPRTRANSFORMER and related parsing rules.
o! Value [2012/08/29] Signature change for function
Db.Value.register_builtin: builtins can now return multiple
states.
o! Value [2012/08/20] Rename Db.Value.assigns_to_zone_inputs_state to
Db.Value.assigns_inputs_to_zone. Add new functions
Db.Value.assigns_outputs_to_zone and
Db.Value.assigns_inputs_to_locations.
o!* Kernel [2012/07/31] Operations that silently mutate AST should now call
Ast.mark_as_changed to clear states depending on it
(fixes #!1244).
-! Inout [2012/07/22] Option -inout-callwise restarts Value when it is
newly set
o! Cil [2012/07/16] Ast changed: Unrool_level renamed into Unroll_specs
and its argument becomes a list for next evolutions.
o! Kernel [2012/07/16] Add function [stmt_can_reach] to the arguments
of Dataflow.Backwards, which is used to speed up the analysis.
See dataflow.mli for good possible values.
-! Rte [2012/07/16] Rename option -rte-const into
-rte-no-trivial-annotations (set by default).
-! Value [2012/07/12] More thorough checks for calls through a function
pointer: warn when the function type and the pointer are
not compatible, and stop when they cannot be reconciled.
-! Kernel [2012/07/12] A negative value given to -ulevel option hides all
UNROLL_LOOP pragmas.
+! Kernel [2012/07/10] Change semantics of 'reachable' properties
for functions. Use intrinsic notion instead of accessibility
of first statement.
o! Kernel [2012/06/25] Correct (albeit slow) hash function for terms
and term lvalues.
-! Kernel [2012/06/22] improve 'reachable' properties.
o! Kernel [2012/06/19] Remove module Inthash. Use Datatype.Int.Hashtbl
instead, or directly carbon2nitrogen.sh migration script.
o! Value [2012/06/18] Made type Ival.tt private.
o! Kernel [2012/06/11] New API for Annotations which merges old
Annotations, Globals.Annotations and operations of Kernel_function
over function contracts.
-! Pdg [2012/06/08] Rename option -dot-pdg into -pdg-dot
o! Kernel [2012/05/30] Kernel.Functions.get does not silently create
a kernel function if it does not already exist. This behavior
is kept for Cil builtins.
o! Kernel [2012/04/26] Plugin.set_optional_help is now deprecated.
*! Kernel [2012/04/14] Introduce more temporaries for a call [lv = f()] if
the return type of f and the type of lv do not match. Fix
issue #1024.
o! Kernel [2012/03/26] Kernel.CppExtraArgs now gets type
Plugin.String_list and not Plugin.String_set (fixed bts #!1132).
-! Kernel [2012/02/29] Adding some more supports for built-in related to
memory blocks.
-! Cil [2012/02/24] Functions returning a value cannot let control flow
falling through the closing '}' Fixes#685.
-! Kernel [2012/02/23] Sets generated assigns clauses into the default
behavior.
-! Kernel [2012/02/08] Adding supports for clause allocates and frees
and their version for loops.
o! Value [2011/12/02] Moved contents of memory_state/Abstract_value
into ai/Lattice_Interval_Set. Use bin/nitrogen2oxygen for
automatic migration.
-*! Kernel [2011/11/07] empty list in complete/disjoint is expanded by
logic type-checker to the list of behavior name of current
contract. Fixes issue #1006. See bts comments for the
differences that can appear in the treatment of specs.
o! Cil [2011/11/04] Add method pFile in printers. Signature change for
Cil.d_file (but you should use !Ast_printer.d_file).
o! Kernel [2011/10/18] Logic_preprocess.file takes an additional parameter,
as gcc pre-processor treats differently .c and .cxx files,
and this must be reflected in annotation pre-processing.
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.
gnomecanvas support.
Actually, it depends completely on lablgtk's gnomecanvas option --
but I didn't manage to check for that. The way I know only works
for inclusion in buildlink3.mk files.
Frama-C is a suite of tools dedicated to the analysis of the source code of
software written in C.
Frama-C gathers several static analysis techniques in a single collaborative
framework. The collaborative approach of Frama-C allows static analyzers to
build upon the results already computed by other analyzers in the framework.
Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer
and dependency analysis.
jaapb
asau
wiz
tonio