CVS commit: pkgsrc/devel/frama-c

["Aleksej Saushev" <asau%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   asau
Date:           Sun Dec 25 15:52:13 UTC 2011

Modified Files:
        pkgsrc/devel/frama-c: Makefile PLIST distinfo options.mk
Removed Files:
        pkgsrc/devel/frama-c: PLIST.gnomecanvas
        pkgsrc/devel/frama-c/patches: patch-aa patch-ab

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.


To generate a diff of this commit:
cvs rdiff -u -r1.15 -r1.16 pkgsrc/devel/frama-c/Makefile
cvs rdiff -u -r1.2 -r1.3 pkgsrc/devel/frama-c/PLIST \
    pkgsrc/devel/frama-c/distinfo pkgsrc/devel/frama-c/options.mk
cvs rdiff -u -r1.1 -r0 pkgsrc/devel/frama-c/PLIST.gnomecanvas
cvs rdiff -u -r1.1.1.1 -r0 pkgsrc/devel/frama-c/patches/patch-aa
cvs rdiff -u -r1.1 -r0 pkgsrc/devel/frama-c/patches/patch-ab

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.