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.

1 files changed, 3 insertions, 7 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index dc7ccb51623..c64a59ab6cf 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.15 2011/12/24 13:18:00 dholland Exp $
+# $NetBSD: Makefile,v 1.16 2011/12/25 15:52:12 asau Exp $
 #
 
-DISTNAME=	frama-c-Beryllium-20090901
-PKGNAME=	${DISTNAME:S/-Beryllium//}
-PKGREVISION=	9
+DISTNAME=	frama-c-Nitrogen-20111001
+PKGNAME=	${DISTNAME:S/-Nitrogen//}
 CATEGORIES=	devel
 MASTER_SITES=	http://frama-c.com/download/
 
@@ -17,11 +16,8 @@ PKG_DESTDIR_SUPPORT=	user-destdir
 USE_TOOLS+=	gmake
 GNU_CONFIGURE=	yes
 
-PLIST_SRC=	${PLIST_SRC_DFLT}
-
 .include "options.mk"
 
-.include "../../x11/gtksourceview/buildlink3.mk"
 .include "../../x11/lablgtk/buildlink3.mk"
 .include "../../lang/ocaml/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"