pkgsrc/devel/frama-c/distinfo

$NetBSD: distinfo,v 1.3 2011/12/25 15:52:12 asau Exp $

SHA1 (frama-c-Nitrogen-20111001.tar.gz) = 5b5b8cd0b21e007012c899ab74bb33cbe23582ed
RMD160 (frama-c-Nitrogen-20111001.tar.gz) = 4401666bdca00c9f8fe9882309116633e5d68984
Size (frama-c-Nitrogen-20111001.tar.gz) = 12110786 bytes
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. 2011-12-25 16:52:12 +01:00			$NetBSD: distinfo,v 1.3 2011/12/25 15:52:12 asau Exp $
import the frama-c source code analysis tool 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. 2009-09-11 17:09:35 +02:00
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. 2011-12-25 16:52:12 +01:00			`SHA1 (frama-c-Nitrogen-20111001.tar.gz) = 5b5b8cd0b21e007012c899ab74bb33cbe23582ed`
			`RMD160 (frama-c-Nitrogen-20111001.tar.gz) = 4401666bdca00c9f8fe9882309116633e5d68984`
			`Size (frama-c-Nitrogen-20111001.tar.gz) = 12110786 bytes`