kpriv/pkgsrc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
pkgsrc/devel/frama-c/Makefile

25 lines
578 B
Makefile
Raw Normal View History

Recursive dependency bump for databases/gdbm ABI_DEPENDS change.
2012-01-24 10:10:50 +01:00
# $NetBSD: Makefile,v 1.18 2012/01/24 09:11:00 sbd 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
DISTNAME= frama-c-Nitrogen-20111001
PKGNAME= ${DISTNAME:S/-Nitrogen//}
Recursive dependency bump for databases/gdbm ABI_DEPENDS change.
2012-01-24 10:10:50 +01:00
PKGREVISION= 2
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
CATEGORIES= devel
Home page and master site moved to http://frama-c.com/
2011-12-23 02:25:08 +01:00
MASTER_SITES= http://frama-c.com/download/
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
MAINTAINER= tonio@NetBSD.org
Home page and master site moved to http://frama-c.com/
2011-12-23 02:25:08 +01:00
HOMEPAGE= http://frama-c.com/
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
COMMENT= Extensible platform dedicated to source-code analysis of C software
LICENSE= gnu-lgpl-v2
PKG_DESTDIR_SUPPORT= user-destdir
USE_TOOLS+= gmake
GNU_CONFIGURE= yes
Add a gnomecanvas option to fix build when lablgtk was compiled without gnomecanvas support. Actually, it depends completely on lablgtk's gnomecanvas option -- but I didn't manage to check for that. The way I know only works for inclusion in buildlink3.mk files.
2009-12-07 17:39:12 +01:00
.include "options.mk"
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
.include "../../x11/lablgtk/buildlink3.mk"
.include "../../lang/ocaml/buildlink3.mk"
.include "../../mk/bsd.pkg.mk"
Reference in a new issue Copy permalink