2012-03-03 01:14:27 by Thomas Klausner | Files touched by this commit (1657) |
Log message:
Recursive bump for pcre-8.30* (shlib major change)
|
2012-02-06 13:42:32 by Thomas Klausner | Files touched by this commit (1812) | |
Log message:
Revbump for
a) tiff update to 4.0 (shlib major change)
b) glib2 update 2.30.2 (adds libffi dependency to buildlink3.mk)
Enjoy.
|
2012-01-24 10:11:18 by Steven Drake | Files touched by this commit (231) |
Log message:
Recursive dependency bump for databases/gdbm ABI_DEPENDS change.
|
2012-01-13 11:55:52 by OBATA Akio | Files touched by this commit (507) |
Log message:
Recursive bump from audio/libaudiofile, x11/qt4-libs and x11/qt4-tools ABI bump.
|
2011-12-25 16:52:13 by Aleksej Saushev | Files touched by this commit (7) |
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.
|
2011-12-24 14:18:00 by David A. Holland | Files touched by this commit (1) |
Log message:
Revert addition of devel/nspr; problem is now solved properly
|
2011-12-23 02:38:20 by Aleksej Saushev | Files touched by this commit (1) |
Log message:
This needs libnspr4.
(This doesn't fix the build yet makes it fail later.)
|
2011-12-23 02:25:08 by Aleksej Saushev | Files touched by this commit (1) |
Log message:
Home page and master site moved to http://frama-c.com/
|
2011-12-06 01:19:26 by Steven Drake | Files touched by this commit (42) |
Log message:
Recursive bump for lang/ocaml buildlink addition.
|
2011-11-01 07:03:15 by Steven Drake | Files touched by this commit (1557) |
Log message:
Recursive bump for graphics/freetype2 buildlink addition.
|