[pkgsrc/trunk]: pkgsrc/devel/frama-c import the frama-c source code analysis ...

[tonio <tonio%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/199d96bcc02b
branches:  trunk
changeset: 564774:199d96bcc02b
user:      tonio <tonio%pkgsrc.org@localhost>
date:      Fri Sep 11 15:09:35 2009 +0000

description:
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.

diffstat:

 devel/frama-c/DESCR            |     8 +
 devel/frama-c/Makefile         |    23 +
 devel/frama-c/PLIST            |   381 ++++++++++++
 devel/frama-c/distinfo         |     6 +
 devel/frama-c/patches/patch-aa |  1213 ++++++++++++++++++++++++++++++++++++++++
 5 files changed, 1631 insertions(+), 0 deletions(-)

diffs (truncated from 1651 to 300 lines):

diff -r d79c7ebe0f87 -r 199d96bcc02b devel/frama-c/DESCR
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/frama-c/DESCR       Fri Sep 11 15:09:35 2009 +0000
@@ -0,0 +1,8 @@
+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.
diff -r d79c7ebe0f87 -r 199d96bcc02b devel/frama-c/Makefile
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/frama-c/Makefile    Fri Sep 11 15:09:35 2009 +0000
@@ -0,0 +1,23 @@
+# $NetBSD: Makefile,v 1.1.1.1 2009/09/11 15:09:35 tonio Exp $
+#
+
+DISTNAME=      frama-c-Beryllium-20090901
+PKGNAME=       ${DISTNAME:S/-Beryllium//}
+CATEGORIES=    devel
+MASTER_SITES=  http://frama-c.cea.fr/download/
+
+MAINTAINER=    tonio%NetBSD.org@localhost
+HOMEPAGE=      http://frama-c.cea.fr/
+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
+
+.include "../../x11/gtksourceview/buildlink3.mk"
+.include "../../graphics/libgnomecanvas/buildlink3.mk"
+.include "../../x11/lablgtk/buildlink3.mk"
+.include "../../lang/ocaml/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"
diff -r d79c7ebe0f87 -r 199d96bcc02b devel/frama-c/PLIST
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/frama-c/PLIST       Fri Sep 11 15:09:35 2009 +0000
@@ -0,0 +1,381 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2009/09/11 15:09:35 tonio Exp $
+bin/caduceus
+bin/frama-c
+bin/frama-c-gui
+bin/frama-c-gui.byte
+bin/frama-c.byte
+bin/gwhy
+bin/gwhy-bin
+bin/jessie
+bin/krakatoa
+bin/rv_merge
+bin/simplify2why
+bin/tool-stat
+bin/why
+bin/why-config
+bin/why-cpulimit
+bin/why-dp
+bin/why-obfuscator
+bin/why-stat
+bin/why2html
+lib/frama-c/about_dialog.cmi
+lib/frama-c/abstract_interp.cmi
+lib/frama-c/abstract_value.cmi
+lib/frama-c/alarms.cmi
+lib/frama-c/alpha.cmi
+lib/frama-c/annotations.cmi
+lib/frama-c/ast.cmi
+lib/frama-c/ast_info.cmi
+lib/frama-c/ast_printer.cmi
+lib/frama-c/availexpslv.cmi
+lib/frama-c/base.cmi
+lib/frama-c/baseUtils.cmi
+lib/frama-c/base_Set_Lattice.cmi
+lib/frama-c/binary_cache.cmi
+lib/frama-c/bit_model_access.cmi
+lib/frama-c/bit_utils.cmi
+lib/frama-c/boot.cmi
+lib/frama-c/buckx.cmi
+lib/frama-c/cabs.cmi
+lib/frama-c/cabs2cil.cmi
+lib/frama-c/cabshelper.cmi
+lib/frama-c/cabsvisit.cmi
+lib/frama-c/callgraph.cmi
+lib/frama-c/cfg.cmi
+lib/frama-c/cil.cmi
+lib/frama-c/cilE.cmi
+lib/frama-c/cil_computation.cmi
+lib/frama-c/cil_const.cmi
+lib/frama-c/cil_datatype.cmi
+lib/frama-c/cil_types.cmi
+lib/frama-c/cilglobopt.cmi
+lib/frama-c/cilmsg.cmi
+lib/frama-c/ciltools.cmi
+lib/frama-c/cilutil.cmi
+lib/frama-c/clexer.cmi
+lib/frama-c/clist.cmi
+lib/frama-c/cmdline.cmi
+lib/frama-c/computation.cmi
+lib/frama-c/concreteModel.cmi
+lib/frama-c/config.cmi
+lib/frama-c/cparser.cmi
+lib/frama-c/cprint.cmi
+lib/frama-c/cvalue_type.cmi
+lib/frama-c/dGraphModel.cmi
+lib/frama-c/dGraphView.cmi
+lib/frama-c/dGraphViewItem.cmi
+lib/frama-c/dataflow.cmi
+lib/frama-c/datatype.cmi
+lib/frama-c/db.cmi
+lib/frama-c/db_types.cmi
+lib/frama-c/deadcodeelim.cmi
+lib/frama-c/debug.cmi
+lib/frama-c/descr.cmi
+lib/frama-c/design.cmi
+lib/frama-c/dominators.cmi
+lib/frama-c/dynamic.cmi
+lib/frama-c/dynlink_common_interface.cmi
+lib/frama-c/errorloc.cmi
+lib/frama-c/escape.cmi
+lib/frama-c/expcompare.cmi
+lib/frama-c/extlib.cmi
+lib/frama-c/file.cmi
+lib/frama-c/filetree.cmi
+lib/frama-c/filter.cmi
+lib/frama-c/frontc.cmi
+lib/frama-c/function_Froms.cmi
+lib/frama-c/globals.cmi
+lib/frama-c/graph.cmi
+lib/frama-c/growArray.cmi
+lib/frama-c/gtk_helper.cmi
+lib/frama-c/gui_init.cmi
+lib/frama-c/hook.cmi
+lib/frama-c/infer_annotations.cmi
+lib/frama-c/inout_type.cmi
+lib/frama-c/int_Base.cmi
+lib/frama-c/int_Interv.cmi
+lib/frama-c/int_Interv_Map.cmi
+lib/frama-c/inthash.cmi
+lib/frama-c/ival.cmi
+lib/frama-c/journal.cmi
+lib/frama-c/kernel.cmi
+lib/frama-c/kernel_function.cmi
+lib/frama-c/kernel_type.cmi
+lib/frama-c/kind.cmi
+lib/frama-c/lattice_With_Isotropy.cmi
+lib/frama-c/launcher.cmi
+lib/frama-c/lexerhack.cmi
+lib/frama-c/liveness.cmi
+lib/frama-c/lmap.cmi
+lib/frama-c/lmap_bitwise.cmi
+lib/frama-c/lmap_whole.cmi
+lib/frama-c/locations.cmi
+lib/frama-c/log.cmi
+lib/frama-c/logic_builtin.cmi
+lib/frama-c/logic_const.cmi
+lib/frama-c/logic_env.cmi
+lib/frama-c/logic_interp.cmi
+lib/frama-c/logic_lexer.cmi
+lib/frama-c/logic_parser.cmi
+lib/frama-c/logic_preprocess.cmi
+lib/frama-c/logic_ptree.cmi
+lib/frama-c/logic_typing.cmi
+lib/frama-c/logic_utils.cmi
+lib/frama-c/loop.cmi
+lib/frama-c/machdep.cmi
+lib/frama-c/machdep_ppc_32.cmi
+lib/frama-c/machdep_ppc_32_diab.cmi
+lib/frama-c/machdep_x86_16.cmi
+lib/frama-c/machdep_x86_32.cmi
+lib/frama-c/machdep_x86_64.cmi
+lib/frama-c/map_Lattice.cmi
+lib/frama-c/mergecil.cmi
+lib/frama-c/mergemap.cmi
+lib/frama-c/messages.cmi
+lib/frama-c/mweak.cmi
+lib/frama-c/my_bigint.cmi
+lib/frama-c/namespace.cmi
+lib/frama-c/new_offsetmap.cmi
+lib/frama-c/obfuscate.cmi
+lib/frama-c/offsetmap.cmi
+lib/frama-c/offsetmap_bitwise.cmi
+lib/frama-c/oneret.cmi
+lib/frama-c/origin.cmi
+lib/frama-c/parameters.cmi
+lib/frama-c/patch.cmi
+lib/frama-c/path_lattice.cmi
+lib/frama-c/pdgIndex.cmi
+lib/frama-c/pdgMarks.cmi
+lib/frama-c/pdgTypes.cmi
+lib/frama-c/plugin.cmi
+lib/frama-c/plugins/Jessie.cma
+lib/frama-c/plugins/Jessie.cmxs
+lib/frama-c/plugins/Ltl_to_acsl.cmo
+lib/frama-c/plugins/Ltl_to_acsl.cmxs
+lib/frama-c/pretty_source.cmi
+lib/frama-c/pretty_utils.cmi
+lib/frama-c/printer.cmi
+lib/frama-c/project.cmi
+lib/frama-c/project_manager.cmi
+lib/frama-c/ptmap.cmi
+lib/frama-c/ptset.cmi
+lib/frama-c/qstack.cmi
+lib/frama-c/rangemap.cmi
+lib/frama-c/reachingdefs.cmi
+lib/frama-c/relations_type.cmi
+lib/frama-c/rmciltmps.cmi
+lib/frama-c/rmtmps.cmi
+lib/frama-c/service_graph.cmi
+lib/frama-c/setWithNearest.cmi
+lib/frama-c/shifted_Location.cmi
+lib/frama-c/signature.cmi
+lib/frama-c/slicingInternals.cmi
+lib/frama-c/slicingTypes.cmi
+lib/frama-c/source_manager.cmi
+lib/frama-c/source_viewer.cmi
+lib/frama-c/special_hooks.cmi
+lib/frama-c/state_set.cmi
+lib/frama-c/stmts_graph.cmi
+lib/frama-c/subst.cmi
+lib/frama-c/translate_lightweight.cmi
+lib/frama-c/type.cmi
+lib/frama-c/unicode.cmi
+lib/frama-c/unmarshal.cmi
+lib/frama-c/unmarshal_nums.cmi
+lib/frama-c/unroll_loops.cmi
+lib/frama-c/usedef.cmi
+lib/frama-c/utf8_logic.cmi
+lib/frama-c/viewGraph.cmi
+lib/frama-c/viewGraph_select.cmi
+lib/frama-c/viewGraph_utils.cmi
+lib/frama-c/visitor.cmi
+lib/frama-c/warning_manager.cmi
+lib/frama-c/whitetrack.cmi
+lib/frama-c/widen.cmi
+lib/frama-c/widen_type.cmi
+lib/frama-c/xDot.cmi
+lib/frama-c/xDotDraw.cmi
+lib/frama-c/zrapp.cmi
+man/man1/frama-c-gui.1
+man/man1/frama-c.1
+man/man1/why.1
+share/frama-c/Makefile.common
+share/frama-c/Makefile.config
+share/frama-c/Makefile.dynamic
+share/frama-c/Makefile.dynamic_config
+share/frama-c/Makefile.plugin
+share/frama-c/builtin.c
+share/frama-c/builtin.h
+share/frama-c/caduceus/coq/caduceus_tactics.v
+share/frama-c/caduceus/coq/caduceus_why.v
+share/frama-c/caduceus/harvey/caduceus_why.rv
+share/frama-c/caduceus/isabelle/caduceus_why.thy
+share/frama-c/caduceus/why/caduceus.why
+share/frama-c/caduceus/why/caduceus_arith.why
+share/frama-c/coq/jessie_why.v
+share/frama-c/fluctuat.h
+share/frama-c/frama-c.rc
+share/frama-c/jessie/assert.h
+share/frama-c/jessie/ctype.h
+share/frama-c/jessie/jc.cmi
+share/frama-c/jessie/jc.cmo
+share/frama-c/jessie/jc.cmx
+share/frama-c/jessie/jc.o
+share/frama-c/jessie/jc_ast.cmi
+share/frama-c/jessie/jc_common_options.cmi
+share/frama-c/jessie/jc_constructors.cmi
+share/frama-c/jessie/jc_env.cmi
+share/frama-c/jessie/jc_envset.cmi
+share/frama-c/jessie/jc_fenv.cmi
+share/frama-c/jessie/jc_iterators.cmi
+share/frama-c/jessie/jc_noutput.cmi
+share/frama-c/jessie/jc_output.cmi
+share/frama-c/jessie/jc_output_misc.cmi
+share/frama-c/jessie/jc_pervasives.cmi
+share/frama-c/jessie/jc_poutput.cmi
+share/frama-c/jessie/jc_region.cmi
+share/frama-c/jessie/jc_stdlib.cmi
+share/frama-c/jessie/jc_type_var.cmi
+share/frama-c/jessie/jessie_exact_prolog.h
+share/frama-c/jessie/jessie_machine_prolog.h
+share/frama-c/jessie/jessie_prolog.h
+share/frama-c/jessie/lib.cmi
+share/frama-c/jessie/loc.cmi
+share/frama-c/jessie/option_misc.cmi
+share/frama-c/jessie/output.cmi
+share/frama-c/jessie/pp.cmi
+share/frama-c/jessie/prolog.c
+share/frama-c/jessie/rc.cmi
+share/frama-c/jessie/stddef.h
+share/frama-c/jessie/stdio.h
+share/frama-c/jessie/stdlib.h
+share/frama-c/jessie/string.h
+share/frama-c/jessie/strings.h
+share/frama-c/jessie/unistd.h
+share/frama-c/jessie/wchar.h
+share/frama-c/libc.c
+share/frama-c/libc.h