head 1.2; access; symbols pkgsrc-2013Q2:1.2.0.6 pkgsrc-2013Q2-base:1.2 pkgsrc-2012Q4:1.2.0.4 pkgsrc-2012Q4-base:1.2 pkgsrc-2011Q4:1.2.0.2 pkgsrc-2011Q4-base:1.2 pkgsrc-2011Q3:1.1.0.12 pkgsrc-2011Q3-base:1.1 pkgsrc-2011Q2:1.1.0.10 pkgsrc-2011Q2-base:1.1 pkgsrc-2011Q1:1.1.0.8 pkgsrc-2011Q1-base:1.1 pkgsrc-2010Q4:1.1.0.6 pkgsrc-2010Q4-base:1.1 pkgsrc-2010Q3:1.1.0.4 pkgsrc-2010Q3-base:1.1 pkgsrc-2010Q2:1.1.0.2 pkgsrc-2010Q2-base:1.1; locks; strict; comment @# @; 1.2 date 2011.12.25.15.52.12; author asau; state dead; branches; next 1.1; 1.1 date 2010.06.15.08.26.54; author wiz; state Exp; branches; next ; desc @@ 1.2 log @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. @ text @$NetBSD: patch-ab,v 1.1 2010/06/15 08:26:54 wiz Exp $ Fix known incompatibility introduced in a recent version of OCaml. The following patch, taken from http://old.nabble.com/Bug-569260:-FTBFS:-expression-was-expected-of-type-string--%3E-string--%3E-string-td27540744.html , fixes it. --- ptests/ptests.ml.orig 2009-08-31 15:38:55.000000000 +0000 +++ ptests/ptests.ml @@@@ -54,7 +54,7 @@@@ module Filename = struct fun a b -> let r = temp_file a b in cygpath r else - temp_file + (fun x y -> temp_file x y) end let default_env var value = @ 1.1 log @Fix build with latest ocaml. From Pascal Cuoq on pkgsrc-users. @ text @d1 1 a1 1 $NetBSD$ @