pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/devel/frama-c
Module Name: pkgsrc
Committed By: dholland
Date: Tue Sep 5 07:30:00 UTC 2017
Modified Files:
pkgsrc/devel/frama-c: Makefile PLIST distinfo options.mk
pkgsrc/devel/frama-c/patches: patch-configure
Added Files:
pkgsrc/devel/frama-c/patches: patch-Makefile
patch-share_Makefile.common patch-src_libraries_utils_c__bindings.c
patch-src_plugins_e-acsl_Makefile patch-src_plugins_wp_configure
patch-src_plugins_wp_configure.ac
patch-src_plugins_wp_share_coqwp_Zbits.v
Log Message:
Update to 20170501 (v15.x, "Phosphorus"). This reflects six major
upstream releases, so visit the HOMEPAGE for further info.
pkgsrc changes:
- old patches were rolled in upstream
- use the ocaml framework
- depends on more ocaml libraries
- depends on lang/coq by default; turn off the coq option to avoid this
XXX: You must build ocamlgraph with ocaml-lablgtk support (which is
XXX: not the default) or the build fails on missing module "Dgraph".
To generate a diff of this commit:
cvs rdiff -u -r1.67 -r1.68 pkgsrc/devel/frama-c/Makefile
cvs rdiff -u -r1.4 -r1.5 pkgsrc/devel/frama-c/PLIST
cvs rdiff -u -r1.6 -r1.7 pkgsrc/devel/frama-c/distinfo
cvs rdiff -u -r1.3 -r1.4 pkgsrc/devel/frama-c/options.mk
cvs rdiff -u -r0 -r1.1 pkgsrc/devel/frama-c/patches/patch-Makefile \
pkgsrc/devel/frama-c/patches/patch-share_Makefile.common \
pkgsrc/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c \
pkgsrc/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile \
pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure \
pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure.ac \
pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v
cvs rdiff -u -r1.1 -r1.2 pkgsrc/devel/frama-c/patches/patch-configure
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: pkgsrc/devel/frama-c/Makefile
diff -u pkgsrc/devel/frama-c/Makefile:1.67 pkgsrc/devel/frama-c/Makefile:1.68
--- pkgsrc/devel/frama-c/Makefile:1.67 Tue Jul 11 14:19:19 2017
+++ pkgsrc/devel/frama-c/Makefile Tue Sep 5 07:30:00 2017
@@ -1,22 +1,28 @@
-# $NetBSD: Makefile,v 1.67 2017/07/11 14:19:19 jaapb Exp $
+# $NetBSD: Makefile,v 1.68 2017/09/05 07:30:00 dholland Exp $
#
-DISTNAME= frama-c-Oxygen-20120901
-PKGNAME= ${DISTNAME:S/-Oxygen//}
-PKGREVISION= 38
+DISTNAME= frama-c-Phosphorus-20170501
+PKGNAME= ${DISTNAME:S/-Phosphorus//}
CATEGORIES= devel
-MASTER_SITES= http://frama-c.com/download/
+MASTER_SITES= https://frama-c.com/download/
MAINTAINER= tonio%NetBSD.org@localhost
-HOMEPAGE= http://frama-c.com/
+HOMEPAGE= https://frama-c.com/
COMMENT= Extensible platform dedicated to source-code analysis of C software
LICENSE= gnu-lgpl-v2
-USE_TOOLS+= gmake
+USE_TOOLS+= gmake autoconf
GNU_CONFIGURE= yes
+OCAML_USE_FINDLIB= yes
+
.include "options.mk"
-.include "../../x11/ocaml-lablgtk/buildlink3.mk"
-.include "../../lang/ocaml/buildlink3.mk"
+# WARNING: you must build ocamlgraph with ocaml-lablgtk support
+# (not the default) or the build fails with missing module "Dgraph".
+
+.include "../../devel/ocamlgraph/buildlink3.mk"
+.include "../../math/ocaml-zarith/buildlink3.mk"
+
+.include "../../mk/ocaml.mk"
.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/devel/frama-c/PLIST
diff -u pkgsrc/devel/frama-c/PLIST:1.4 pkgsrc/devel/frama-c/PLIST:1.5
--- pkgsrc/devel/frama-c/PLIST:1.4 Mon Oct 8 15:28:04 2012
+++ pkgsrc/devel/frama-c/PLIST Tue Sep 5 07:30:00 2017
@@ -1,57 +1,32 @@
-@comment $NetBSD: PLIST,v 1.4 2012/10/08 15:28:04 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.5 2017/09/05 07:30:00 dholland Exp $
+bin/e-acsl-gcc.sh
bin/frama-c
+bin/frama-c-config
${PLIST.gui}bin/frama-c-gui
${PLIST.gui}bin/frama-c-gui.byte
bin/frama-c.byte
-bin/ptests.byte
-lib/frama-c/Constant_Propagation.cmo
-lib/frama-c/Constant_Propagation.cmx
-lib/frama-c/Constant_Propagation.o
-lib/frama-c/From.cmo
-lib/frama-c/From.cmx
-lib/frama-c/From.o
-lib/frama-c/Impact.cmo
-lib/frama-c/Impact.cmx
-lib/frama-c/Impact.o
-lib/frama-c/Inout.cmo
-lib/frama-c/Inout.cmx
-lib/frama-c/Inout.o
-lib/frama-c/Metrics.cmo
-lib/frama-c/Metrics.cmx
-lib/frama-c/Metrics.o
-lib/frama-c/Occurrence.cmo
-lib/frama-c/Occurrence.cmx
-lib/frama-c/Occurrence.o
-lib/frama-c/Pdg.cmo
-lib/frama-c/Pdg.cmx
-lib/frama-c/Pdg.o
-lib/frama-c/Postdominators.cmo
-lib/frama-c/Postdominators.cmx
-lib/frama-c/Postdominators.o
-lib/frama-c/RteGen.cmo
-lib/frama-c/RteGen.cmx
-lib/frama-c/RteGen.o
-lib/frama-c/Scope.cmo
-lib/frama-c/Scope.cmx
-lib/frama-c/Scope.o
-lib/frama-c/Semantic_callgraph.cmo
-lib/frama-c/Semantic_callgraph.cmx
-lib/frama-c/Semantic_callgraph.o
-lib/frama-c/Slicing.cmo
-lib/frama-c/Slicing.cmx
-lib/frama-c/Slicing.o
-lib/frama-c/Sparecode.cmo
-lib/frama-c/Sparecode.cmx
-lib/frama-c/Sparecode.o
-lib/frama-c/Syntactic_callgraph.cmo
-lib/frama-c/Syntactic_callgraph.cmx
-lib/frama-c/Syntactic_callgraph.o
-lib/frama-c/Users.cmo
-lib/frama-c/Users.cmx
-lib/frama-c/Users.o
-lib/frama-c/Value.cmo
-lib/frama-c/Value.cmx
-lib/frama-c/Value.o
+@comment bin/ptests.byte
+bin/ptests.opt
+lib/frama-c/FCBuffer.cmi
+lib/frama-c/FCBuffer.cmo
+lib/frama-c/FCBuffer.cmx
+lib/frama-c/FCBuffer.o
+lib/frama-c/FCHashtbl.cmi
+lib/frama-c/FCHashtbl.cmo
+lib/frama-c/FCHashtbl.cmx
+lib/frama-c/FCHashtbl.o
+lib/frama-c/FCMap.cmi
+lib/frama-c/FCMap.cmo
+lib/frama-c/FCMap.cmx
+lib/frama-c/FCMap.o
+lib/frama-c/FCSet.cmi
+lib/frama-c/FCSet.cmo
+lib/frama-c/FCSet.cmx
+lib/frama-c/FCSet.o
+lib/frama-c/Qed.cmi
+lib/frama-c/Qed.cmo
+lib/frama-c/Qed.cmx
+lib/frama-c/Qed.o
lib/frama-c/abstract_interp.cmi
lib/frama-c/abstract_interp.cmo
lib/frama-c/abstract_interp.cmx
@@ -80,6 +55,10 @@ lib/frama-c/annotations.cmi
lib/frama-c/annotations.cmo
lib/frama-c/annotations.cmx
lib/frama-c/annotations.o
+lib/frama-c/asm_contracts.cmi
+lib/frama-c/asm_contracts.cmo
+lib/frama-c/asm_contracts.cmx
+lib/frama-c/asm_contracts.o
lib/frama-c/ast.cmi
lib/frama-c/ast.cmo
lib/frama-c/ast.cmx
@@ -88,14 +67,6 @@ lib/frama-c/ast_info.cmi
lib/frama-c/ast_info.cmo
lib/frama-c/ast_info.cmx
lib/frama-c/ast_info.o
-lib/frama-c/ast_printer.cmi
-lib/frama-c/ast_printer.cmo
-lib/frama-c/ast_printer.cmx
-lib/frama-c/ast_printer.o
-lib/frama-c/availexpslv.cmi
-lib/frama-c/availexpslv.cmo
-lib/frama-c/availexpslv.cmx
-lib/frama-c/availexpslv.o
lib/frama-c/bag.cmi
lib/frama-c/bag.cmo
lib/frama-c/bag.cmx
@@ -104,18 +75,10 @@ lib/frama-c/base.cmi
lib/frama-c/base.cmo
lib/frama-c/base.cmx
lib/frama-c/base.o
-lib/frama-c/base_Set_Lattice.cmi
-lib/frama-c/base_Set_Lattice.cmo
-lib/frama-c/base_Set_Lattice.cmx
-lib/frama-c/base_Set_Lattice.o
lib/frama-c/binary_cache.cmi
lib/frama-c/binary_cache.cmo
lib/frama-c/binary_cache.cmx
lib/frama-c/binary_cache.o
-lib/frama-c/bit_model_access.cmi
-lib/frama-c/bit_model_access.cmo
-lib/frama-c/bit_model_access.cmx
-lib/frama-c/bit_model_access.o
lib/frama-c/bit_utils.cmi
lib/frama-c/bit_utils.cmo
lib/frama-c/bit_utils.cmx
@@ -132,11 +95,11 @@ lib/frama-c/boot.cmi
lib/frama-c/boot.cmo
lib/frama-c/boot.cmx
lib/frama-c/boot.o
-lib/frama-c/buckx.cmi
-lib/frama-c/buckx.cmo
-lib/frama-c/buckx.cmx
-lib/frama-c/buckx.o
-lib/frama-c/buckx_c.o
+lib/frama-c/bottom.cmi
+lib/frama-c/bottom.cmo
+lib/frama-c/bottom.cmx
+lib/frama-c/bottom.o
+lib/frama-c/c_bindings.o
lib/frama-c/cabs.cmi
lib/frama-c/cabs.cmo
lib/frama-c/cabs.cmx
@@ -145,14 +108,10 @@ lib/frama-c/cabs2cil.cmi
lib/frama-c/cabs2cil.cmo
lib/frama-c/cabs2cil.cmx
lib/frama-c/cabs2cil.o
-lib/frama-c/cabsbranches.cmi
-lib/frama-c/cabsbranches.cmo
-lib/frama-c/cabsbranches.cmx
-lib/frama-c/cabsbranches.o
-lib/frama-c/cabscond.cmi
-lib/frama-c/cabscond.cmo
-lib/frama-c/cabscond.cmx
-lib/frama-c/cabscond.o
+lib/frama-c/cabs_debug.cmi
+lib/frama-c/cabs_debug.cmo
+lib/frama-c/cabs_debug.cmx
+lib/frama-c/cabs_debug.o
lib/frama-c/cabshelper.cmi
lib/frama-c/cabshelper.cmo
lib/frama-c/cabshelper.cmx
@@ -161,10 +120,6 @@ lib/frama-c/cabsvisit.cmi
lib/frama-c/cabsvisit.cmo
lib/frama-c/cabsvisit.cmx
lib/frama-c/cabsvisit.o
-lib/frama-c/callgraph.cmi
-lib/frama-c/callgraph.cmo
-lib/frama-c/callgraph.cmx
-lib/frama-c/callgraph.o
lib/frama-c/cfg.cmi
lib/frama-c/cfg.cmo
lib/frama-c/cfg.cmx
@@ -185,35 +140,35 @@ lib/frama-c/cil_datatype.cmi
lib/frama-c/cil_datatype.cmo
lib/frama-c/cil_datatype.cmx
lib/frama-c/cil_datatype.o
+lib/frama-c/cil_descriptive_printer.cmi
+lib/frama-c/cil_descriptive_printer.cmo
+lib/frama-c/cil_descriptive_printer.cmx
+lib/frama-c/cil_descriptive_printer.o
+lib/frama-c/cil_printer.cmi
+lib/frama-c/cil_printer.cmo
+lib/frama-c/cil_printer.cmx
+lib/frama-c/cil_printer.o
lib/frama-c/cil_state_builder.cmi
lib/frama-c/cil_state_builder.cmo
lib/frama-c/cil_state_builder.cmx
lib/frama-c/cil_state_builder.o
lib/frama-c/cil_types.cmi
-lib/frama-c/cilglobopt.cmi
-lib/frama-c/cilglobopt.cmo
-lib/frama-c/cilglobopt.cmx
-lib/frama-c/cilglobopt.o
-lib/frama-c/cilmsg.cmi
-lib/frama-c/cilmsg.cmo
-lib/frama-c/cilmsg.cmx
-lib/frama-c/cilmsg.o
-@comment lib/frama-c/ciltools.cmi
-@comment lib/frama-c/ciltools.cmo
-@comment lib/frama-c/ciltools.cmx
-@comment lib/frama-c/ciltools.o
-lib/frama-c/cilutil.cmi
-lib/frama-c/cilutil.cmo
-lib/frama-c/cilutil.cmx
-lib/frama-c/cilutil.o
+lib/frama-c/cil_types_debug.cmi
+lib/frama-c/cil_types_debug.cmo
+lib/frama-c/cil_types_debug.cmx
+lib/frama-c/cil_types_debug.o
+lib/frama-c/cilconfig.cmi
+lib/frama-c/cilconfig.cmo
+lib/frama-c/cilconfig.cmx
+lib/frama-c/cilconfig.o
lib/frama-c/clexer.cmi
lib/frama-c/clexer.cmo
lib/frama-c/clexer.cmx
lib/frama-c/clexer.o
-lib/frama-c/clist.cmi
-lib/frama-c/clist.cmo
-lib/frama-c/clist.cmx
-lib/frama-c/clist.o
+lib/frama-c/clone.cmi
+lib/frama-c/clone.cmo
+lib/frama-c/clone.cmx
+lib/frama-c/clone.o
lib/frama-c/cmdline.cmi
lib/frama-c/cmdline.cmo
lib/frama-c/cmdline.cmx
@@ -246,6 +201,14 @@ lib/frama-c/dataflow.cmi
lib/frama-c/dataflow.cmo
lib/frama-c/dataflow.cmx
lib/frama-c/dataflow.o
+lib/frama-c/dataflow2.cmi
+lib/frama-c/dataflow2.cmo
+lib/frama-c/dataflow2.cmx
+lib/frama-c/dataflow2.o
+lib/frama-c/dataflows.cmi
+lib/frama-c/dataflows.cmo
+lib/frama-c/dataflows.cmx
+lib/frama-c/dataflows.o
lib/frama-c/datatype.cmi
lib/frama-c/datatype.cmo
lib/frama-c/datatype.cmx
@@ -254,10 +217,6 @@ lib/frama-c/db.cmi
lib/frama-c/db.cmo
lib/frama-c/db.cmx
lib/frama-c/db.o
-lib/frama-c/deadcodeelim.cmi
-lib/frama-c/deadcodeelim.cmo
-lib/frama-c/deadcodeelim.cmx
-lib/frama-c/deadcodeelim.o
${PLIST.gui}lib/frama-c/debug_manager.cmi
${PLIST.gui}lib/frama-c/debug_manager.cmo
${PLIST.gui}lib/frama-c/debug_manager.cmx
@@ -274,7 +233,10 @@ ${PLIST.gui}lib/frama-c/design.cmi
${PLIST.gui}lib/frama-c/design.cmo
${PLIST.gui}lib/frama-c/design.cmx
${PLIST.gui}lib/frama-c/design.o
-${PLIST.gui}lib/frama-c/dgraph.cmi
+lib/frama-c/destructors.cmi
+lib/frama-c/destructors.cmo
+lib/frama-c/destructors.cmx
+lib/frama-c/destructors.o
lib/frama-c/dominators.cmi
lib/frama-c/dominators.cmo
lib/frama-c/dominators.cmx
@@ -283,10 +245,6 @@ lib/frama-c/dynamic.cmi
lib/frama-c/dynamic.cmo
lib/frama-c/dynamic.cmx
lib/frama-c/dynamic.o
-lib/frama-c/dynlink_common_interface.cmi
-lib/frama-c/dynlink_common_interface.cmo
-lib/frama-c/dynlink_common_interface.cmx
-lib/frama-c/dynlink_common_interface.o
lib/frama-c/emitter.cmi
lib/frama-c/emitter.cmo
lib/frama-c/emitter.cmx
@@ -299,10 +257,10 @@ lib/frama-c/escape.cmi
lib/frama-c/escape.cmo
lib/frama-c/escape.cmx
lib/frama-c/escape.o
-lib/frama-c/expcompare.cmi
-lib/frama-c/expcompare.cmo
-lib/frama-c/expcompare.cmx
-lib/frama-c/expcompare.o
+lib/frama-c/exn_flow.cmi
+lib/frama-c/exn_flow.cmo
+lib/frama-c/exn_flow.cmx
+lib/frama-c/exn_flow.o
lib/frama-c/extlib.cmi
lib/frama-c/extlib.cmo
lib/frama-c/extlib.cmx
@@ -315,6 +273,14 @@ ${PLIST.gui}lib/frama-c/file_manager.cmi
${PLIST.gui}lib/frama-c/file_manager.cmo
${PLIST.gui}lib/frama-c/file_manager.cmx
${PLIST.gui}lib/frama-c/file_manager.o
+lib/frama-c/filecheck.cmi
+lib/frama-c/filecheck.cmo
+lib/frama-c/filecheck.cmx
+lib/frama-c/filecheck.o
+lib/frama-c/filepath.cmi
+lib/frama-c/filepath.cmo
+lib/frama-c/filepath.cmx
+lib/frama-c/filepath.o
${PLIST.gui}lib/frama-c/filetree.cmi
${PLIST.gui}lib/frama-c/filetree.cmo
${PLIST.gui}lib/frama-c/filetree.cmx
@@ -327,6 +293,10 @@ lib/frama-c/floating_point.cmi
lib/frama-c/floating_point.cmo
lib/frama-c/floating_point.cmx
lib/frama-c/floating_point.o
+lib/frama-c/frama_c_init.cmi
+lib/frama-c/frama_c_init.cmo
+lib/frama-c/frama_c_init.cmx
+lib/frama-c/frama_c_init.o
lib/frama-c/frontc.cmi
lib/frama-c/frontc.cmo
lib/frama-c/frontc.cmx
@@ -335,18 +305,14 @@ lib/frama-c/function_Froms.cmi
lib/frama-c/function_Froms.cmo
lib/frama-c/function_Froms.cmx
lib/frama-c/function_Froms.o
+lib/frama-c/fval.cmi
+lib/frama-c/fval.cmo
+lib/frama-c/fval.cmx
+lib/frama-c/fval.o
lib/frama-c/globals.cmi
lib/frama-c/globals.cmo
lib/frama-c/globals.cmx
lib/frama-c/globals.o
-lib/frama-c/graph.cmi
-lib/frama-c/graph.cmo
-lib/frama-c/graph.cmx
-lib/frama-c/graph.o
-lib/frama-c/growArray.cmi
-lib/frama-c/growArray.cmo
-lib/frama-c/growArray.cmx
-lib/frama-c/growArray.o
${PLIST.gui}lib/frama-c/gtk_form.cmi
${PLIST.gui}lib/frama-c/gtk_form.cmo
${PLIST.gui}lib/frama-c/gtk_form.cmx
@@ -355,11 +321,14 @@ ${PLIST.gui}lib/frama-c/gtk_helper.cmi
${PLIST.gui}lib/frama-c/gtk_helper.cmo
${PLIST.gui}lib/frama-c/gtk_helper.cmx
${PLIST.gui}lib/frama-c/gtk_helper.o
-${PLIST.gui}lib/frama-c/gui_init.cmi
${PLIST.gui}lib/frama-c/gui_parameters.cmi
${PLIST.gui}lib/frama-c/gui_parameters.cmo
${PLIST.gui}lib/frama-c/gui_parameters.cmx
${PLIST.gui}lib/frama-c/gui_parameters.o
+${PLIST.gui}lib/frama-c/gui_printers.cmi
+${PLIST.gui}lib/frama-c/gui_printers.cmo
+${PLIST.gui}lib/frama-c/gui_printers.cmx
+${PLIST.gui}lib/frama-c/gui_printers.o
${PLIST.gui}lib/frama-c/help_manager.cmi
${PLIST.gui}lib/frama-c/help_manager.cmo
${PLIST.gui}lib/frama-c/help_manager.cmx
@@ -368,10 +337,6 @@ ${PLIST.gui}lib/frama-c/history.cmi
${PLIST.gui}lib/frama-c/history.cmo
${PLIST.gui}lib/frama-c/history.cmx
${PLIST.gui}lib/frama-c/history.o
-lib/frama-c/hashtbl_common_interface.cmi
-lib/frama-c/hashtbl_common_interface.cmo
-lib/frama-c/hashtbl_common_interface.cmx
-lib/frama-c/hashtbl_common_interface.o
lib/frama-c/hook.cmi
lib/frama-c/hook.cmo
lib/frama-c/hook.cmx
@@ -380,6 +345,7 @@ lib/frama-c/hptmap.cmi
lib/frama-c/hptmap.cmo
lib/frama-c/hptmap.cmx
lib/frama-c/hptmap.o
+lib/frama-c/hptmap_sig.cmi
lib/frama-c/hptset.cmi
lib/frama-c/hptset.cmo
lib/frama-c/hptset.cmx
@@ -400,14 +366,15 @@ lib/frama-c/int_Base.cmi
lib/frama-c/int_Base.cmo
lib/frama-c/int_Base.cmx
lib/frama-c/int_Base.o
-lib/frama-c/int_Interv.cmi
-lib/frama-c/int_Interv.cmo
-lib/frama-c/int_Interv.cmx
-lib/frama-c/int_Interv.o
-lib/frama-c/int_Interv_Map.cmi
-lib/frama-c/int_Interv_Map.cmo
-lib/frama-c/int_Interv_Map.cmx
-lib/frama-c/int_Interv_Map.o
+lib/frama-c/int_Intervals.cmi
+lib/frama-c/int_Intervals.cmo
+lib/frama-c/int_Intervals.cmx
+lib/frama-c/int_Intervals.o
+lib/frama-c/int_Intervals_sig.cmi
+lib/frama-c/integer.cmi
+lib/frama-c/integer.cmo
+lib/frama-c/integer.cmx
+lib/frama-c/integer.o
@comment lib/frama-c/inthash.cmi
@comment lib/frama-c/inthash.cmo
@comment lib/frama-c/inthash.cmx
@@ -420,6 +387,10 @@ lib/frama-c/journal.cmi
lib/frama-c/journal.cmo
lib/frama-c/journal.cmx
lib/frama-c/journal.o
+lib/frama-c/json.cmi
+lib/frama-c/json.cmo
+lib/frama-c/json.cmx
+lib/frama-c/json.o
lib/frama-c/kernel.cmi
lib/frama-c/kernel.cmo
lib/frama-c/kernel.cmx
@@ -428,23 +399,23 @@ lib/frama-c/kernel_function.cmi
lib/frama-c/kernel_function.cmo
lib/frama-c/kernel_function.cmx
lib/frama-c/kernel_function.o
-lib/frama-c/lattice_Interval_Set.cmi
-lib/frama-c/lattice_Interval_Set.cmo
-lib/frama-c/lattice_Interval_Set.cmx
-lib/frama-c/lattice_Interval_Set.o
-lib/frama-c/lattice_With_Isotropy.cmi
+lib/frama-c/lattice_messages.cmi
+lib/frama-c/lattice_messages.cmo
+lib/frama-c/lattice_messages.cmx
+lib/frama-c/lattice_messages.o
+lib/frama-c/lattice_type.cmi
${PLIST.gui}lib/frama-c/launcher.cmi
${PLIST.gui}lib/frama-c/launcher.cmo
${PLIST.gui}lib/frama-c/launcher.cmx
${PLIST.gui}lib/frama-c/launcher.o
+lib/frama-c/leftistheap.cmi
+lib/frama-c/leftistheap.cmo
+lib/frama-c/leftistheap.cmx
+lib/frama-c/leftistheap.o
lib/frama-c/lexerhack.cmi
lib/frama-c/lexerhack.cmo
lib/frama-c/lexerhack.cmx
lib/frama-c/lexerhack.o
-lib/frama-c/liveness.cmi
-lib/frama-c/liveness.cmo
-lib/frama-c/liveness.cmx
-lib/frama-c/liveness.o
lib/frama-c/lmap.cmi
lib/frama-c/lmap.cmo
lib/frama-c/lmap.cmx
@@ -453,6 +424,7 @@ lib/frama-c/lmap_bitwise.cmi
lib/frama-c/lmap_bitwise.cmo
lib/frama-c/lmap_bitwise.cmx
lib/frama-c/lmap_bitwise.o
+lib/frama-c/lmap_sig.cmi
lib/frama-c/locations.cmi
lib/frama-c/locations.cmo
lib/frama-c/locations.cmx
@@ -506,34 +478,14 @@ lib/frama-c/loop.cmi
lib/frama-c/loop.cmo
lib/frama-c/loop.cmx
lib/frama-c/loop.o
-lib/frama-c/machdep.cmi
-lib/frama-c/machdep.cmo
-lib/frama-c/machdep.cmx
-lib/frama-c/machdep.o
-lib/frama-c/machdep_ppc_32.cmi
-lib/frama-c/machdep_ppc_32.cmo
-lib/frama-c/machdep_ppc_32.cmx
-lib/frama-c/machdep_ppc_32.o
-lib/frama-c/machdep_x86_16.cmi
-lib/frama-c/machdep_x86_16.cmo
-lib/frama-c/machdep_x86_16.cmx
-lib/frama-c/machdep_x86_16.o
-lib/frama-c/machdep_x86_32.cmi
-lib/frama-c/machdep_x86_32.cmo
-lib/frama-c/machdep_x86_32.cmx
-lib/frama-c/machdep_x86_32.o
-lib/frama-c/machdep_x86_64.cmi
-lib/frama-c/machdep_x86_64.cmo
-lib/frama-c/machdep_x86_64.cmx
-lib/frama-c/machdep_x86_64.o
+lib/frama-c/machdeps.cmi
+lib/frama-c/machdeps.cmo
+lib/frama-c/machdeps.cmx
+lib/frama-c/machdeps.o
lib/frama-c/map_Lattice.cmi
lib/frama-c/map_Lattice.cmo
lib/frama-c/map_Lattice.cmx
lib/frama-c/map_Lattice.o
-lib/frama-c/map_common_interface.cmi
-lib/frama-c/map_common_interface.cmo
-lib/frama-c/map_common_interface.cmx
-lib/frama-c/map_common_interface.o
${PLIST.gui}lib/frama-c/menu_manager.cmi
${PLIST.gui}lib/frama-c/menu_manager.cmo
${PLIST.gui}lib/frama-c/menu_manager.cmx
@@ -546,39 +498,42 @@ lib/frama-c/messages.cmi
lib/frama-c/messages.cmo
lib/frama-c/messages.cmx
lib/frama-c/messages.o
-lib/frama-c/my_bigint.cmi
-lib/frama-c/my_bigint.cmo
-lib/frama-c/my_bigint.cmx
-lib/frama-c/my_bigint.o
-lib/frama-c/mybigarray.o
-lib/frama-c/new_offsetmap.cmi
-lib/frama-c/new_offsetmap.cmo
-lib/frama-c/new_offsetmap.cmx
-lib/frama-c/new_offsetmap.o
-lib/frama-c/obfuscate.cmi
-lib/frama-c/obfuscate.cmo
-lib/frama-c/obfuscate.cmx
-lib/frama-c/obfuscate.o
lib/frama-c/offsetmap.cmi
lib/frama-c/offsetmap.cmo
lib/frama-c/offsetmap.cmx
lib/frama-c/offsetmap.o
-lib/frama-c/offsetmap_bitwise.cmi
-lib/frama-c/offsetmap_bitwise.cmo
-lib/frama-c/offsetmap_bitwise.cmx
-lib/frama-c/offsetmap_bitwise.o
+lib/frama-c/offsetmap_bitwise_sig.cmi
+lib/frama-c/offsetmap_lattice_with_isotropy.cmi
+lib/frama-c/offsetmap_sig.cmi
lib/frama-c/oneret.cmi
lib/frama-c/oneret.cmo
lib/frama-c/oneret.cmx
lib/frama-c/oneret.o
+lib/frama-c/ordered_stmt.cmi
+lib/frama-c/ordered_stmt.cmo
+lib/frama-c/ordered_stmt.cmx
+lib/frama-c/ordered_stmt.o
lib/frama-c/origin.cmi
lib/frama-c/origin.cmo
lib/frama-c/origin.cmx
lib/frama-c/origin.o
-lib/frama-c/parameter.cmi
-lib/frama-c/parameter.cmo
-lib/frama-c/parameter.cmx
-lib/frama-c/parameter.o
+lib/frama-c/parameter_builder.cmi
+lib/frama-c/parameter_builder.cmo
+lib/frama-c/parameter_builder.cmx
+lib/frama-c/parameter_builder.o
+lib/frama-c/parameter_category.cmi
+lib/frama-c/parameter_category.cmo
+lib/frama-c/parameter_category.cmx
+lib/frama-c/parameter_category.o
+lib/frama-c/parameter_customize.cmi
+lib/frama-c/parameter_customize.cmo
+lib/frama-c/parameter_customize.cmx
+lib/frama-c/parameter_customize.o
+lib/frama-c/parameter_sig.cmi
+lib/frama-c/parameter_state.cmi
+lib/frama-c/parameter_state.cmo
+lib/frama-c/parameter_state.cmx
+lib/frama-c/parameter_state.o
@comment lib/frama-c/path_lattice.cmi
@comment lib/frama-c/path_lattice.cmo
@comment lib/frama-c/path_lattice.cmx
@@ -600,28 +555,166 @@ lib/frama-c/plugin.cmo
lib/frama-c/plugin.cmx
lib/frama-c/plugin.o
lib/frama-c/plugins/Aorai.cmi
-lib/frama-c/plugins/Aorai.cmo
-lib/frama-c/plugins/Aorai.cmxs
+lib/frama-c/plugins/Callgraph.cmi
+lib/frama-c/plugins/Constant_Propagation.cmi
+lib/frama-c/plugins/E_ACSL.cmi
+lib/frama-c/plugins/From.cmi
+lib/frama-c/plugins/Impact.cmi
+lib/frama-c/plugins/Inout.cmi
+lib/frama-c/plugins/LoopAnalysis.cmi
+lib/frama-c/plugins/META.frama-c-aorai
+lib/frama-c/plugins/META.frama-c-callgraph
+lib/frama-c/plugins/META.frama-c-constant_propagation
+lib/frama-c/plugins/META.frama-c-e_acsl
+lib/frama-c/plugins/META.frama-c-from
+lib/frama-c/plugins/META.frama-c-impact
+lib/frama-c/plugins/META.frama-c-inout
+lib/frama-c/plugins/META.frama-c-loopanalysis
+lib/frama-c/plugins/META.frama-c-metrics
+lib/frama-c/plugins/META.frama-c-nonterm
+lib/frama-c/plugins/META.frama-c-obfuscator
+lib/frama-c/plugins/META.frama-c-occurrence
+lib/frama-c/plugins/META.frama-c-pdg
+lib/frama-c/plugins/META.frama-c-postdominators
+lib/frama-c/plugins/META.frama-c-print_api
+lib/frama-c/plugins/META.frama-c-report
+lib/frama-c/plugins/META.frama-c-rtegen
+lib/frama-c/plugins/META.frama-c-scope
+lib/frama-c/plugins/META.frama-c-security_slicing
+lib/frama-c/plugins/META.frama-c-slicing
+lib/frama-c/plugins/META.frama-c-sparecode
+lib/frama-c/plugins/META.frama-c-users
+lib/frama-c/plugins/META.frama-c-value
+lib/frama-c/plugins/META.frama-c-variadic
+lib/frama-c/plugins/META.frama-c-wp
+lib/frama-c/plugins/Metrics.cmi
+lib/frama-c/plugins/Nonterm.cmi
lib/frama-c/plugins/Obfuscator.cmi
-lib/frama-c/plugins/Obfuscator.cmo
-lib/frama-c/plugins/Obfuscator.cmxs
+lib/frama-c/plugins/Occurrence.cmi
+lib/frama-c/plugins/Pdg.cmi
+lib/frama-c/plugins/Postdominators.cmi
+lib/frama-c/plugins/Print_api.cmi
lib/frama-c/plugins/Report.cmi
-lib/frama-c/plugins/Report.cmo
-lib/frama-c/plugins/Report.cmxs
+lib/frama-c/plugins/RteGen.cmi
+lib/frama-c/plugins/Scope.cmi
lib/frama-c/plugins/Security_slicing.cmi
-lib/frama-c/plugins/Security_slicing.cmo
-lib/frama-c/plugins/Security_slicing.cmxs
-lib/frama-c/plugins/Wp.cma
+lib/frama-c/plugins/Slicing.cmi
+lib/frama-c/plugins/Sparecode.cmi
+lib/frama-c/plugins/Users.cmi
+lib/frama-c/plugins/Value.cmi
+lib/frama-c/plugins/Variadic.cmi
lib/frama-c/plugins/Wp.cmi
-@comment lib/frama-c/plugins/Wp.cmo
-lib/frama-c/plugins/Wp.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Callgraph.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Callgraph.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Callgraph.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/From.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/From.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/From.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Impact.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Impact.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Impact.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Metrics.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Metrics.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Metrics.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Occurrence.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Occurrence.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Occurrence.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Scope.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Scope.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Scope.cmxs
${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmi
${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmo
${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Slicing.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Slicing.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Slicing.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Value.cmi
+${PLIST.gui}lib/frama-c/plugins/gui/Value.cmo
+${PLIST.gui}lib/frama-c/plugins/gui/Value.cmxs
${PLIST.gui}lib/frama-c/plugins/gui/Wp.cma
${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmi
@comment ${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmo
${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmxs
+lib/frama-c/plugins/top/Aorai.cmo
+lib/frama-c/plugins/top/Aorai.cmx
+lib/frama-c/plugins/top/Aorai.cmxs
+lib/frama-c/plugins/top/Callgraph.cmo
+lib/frama-c/plugins/top/Callgraph.cmx
+lib/frama-c/plugins/top/Callgraph.cmxs
+lib/frama-c/plugins/top/Constant_Propagation.cmo
+lib/frama-c/plugins/top/Constant_Propagation.cmx
+lib/frama-c/plugins/top/Constant_Propagation.cmxs
+lib/frama-c/plugins/top/E_ACSL.cmo
+lib/frama-c/plugins/top/E_ACSL.cmx
+lib/frama-c/plugins/top/E_ACSL.cmxs
+lib/frama-c/plugins/top/From.cmo
+lib/frama-c/plugins/top/From.cmx
+lib/frama-c/plugins/top/From.cmxs
+lib/frama-c/plugins/top/Impact.cmo
+lib/frama-c/plugins/top/Impact.cmx
+lib/frama-c/plugins/top/Impact.cmxs
+lib/frama-c/plugins/top/Inout.cmo
+lib/frama-c/plugins/top/Inout.cmx
+lib/frama-c/plugins/top/Inout.cmxs
+lib/frama-c/plugins/top/LoopAnalysis.cmo
+lib/frama-c/plugins/top/LoopAnalysis.cmx
+lib/frama-c/plugins/top/LoopAnalysis.cmxs
+lib/frama-c/plugins/top/Metrics.cmo
+lib/frama-c/plugins/top/Metrics.cmx
+lib/frama-c/plugins/top/Metrics.cmxs
+lib/frama-c/plugins/top/Nonterm.cmo
+lib/frama-c/plugins/top/Nonterm.cmx
+lib/frama-c/plugins/top/Nonterm.cmxs
+lib/frama-c/plugins/top/Obfuscator.cmo
+lib/frama-c/plugins/top/Obfuscator.cmx
+lib/frama-c/plugins/top/Obfuscator.cmxs
+lib/frama-c/plugins/top/Occurrence.cmo
+lib/frama-c/plugins/top/Occurrence.cmx
+lib/frama-c/plugins/top/Occurrence.cmxs
+lib/frama-c/plugins/top/Pdg.cmo
+lib/frama-c/plugins/top/Pdg.cmx
+lib/frama-c/plugins/top/Pdg.cmxs
+lib/frama-c/plugins/top/Postdominators.cmo
+lib/frama-c/plugins/top/Postdominators.cmx
+lib/frama-c/plugins/top/Postdominators.cmxs
+lib/frama-c/plugins/top/Print_api.cmo
+lib/frama-c/plugins/top/Print_api.cmx
+lib/frama-c/plugins/top/Print_api.cmxs
+lib/frama-c/plugins/top/Report.cmo
+lib/frama-c/plugins/top/Report.cmx
+lib/frama-c/plugins/top/Report.cmxs
+lib/frama-c/plugins/top/RteGen.cmo
+lib/frama-c/plugins/top/RteGen.cmx
+lib/frama-c/plugins/top/RteGen.cmxs
+lib/frama-c/plugins/top/Scope.cmo
+lib/frama-c/plugins/top/Scope.cmx
+lib/frama-c/plugins/top/Scope.cmxs
+lib/frama-c/plugins/top/Security_slicing.cmo
+lib/frama-c/plugins/top/Security_slicing.cmx
+lib/frama-c/plugins/top/Security_slicing.cmxs
+lib/frama-c/plugins/top/Slicing.cmo
+lib/frama-c/plugins/top/Slicing.cmx
+lib/frama-c/plugins/top/Slicing.cmxs
+lib/frama-c/plugins/top/Sparecode.cmo
+lib/frama-c/plugins/top/Sparecode.cmx
+lib/frama-c/plugins/top/Sparecode.cmxs
+lib/frama-c/plugins/top/Users.cmo
+lib/frama-c/plugins/top/Users.cmx
+lib/frama-c/plugins/top/Users.cmxs
+lib/frama-c/plugins/top/Value.cmo
+lib/frama-c/plugins/top/Value.cmx
+lib/frama-c/plugins/top/Value.cmxs
+lib/frama-c/plugins/top/Variadic.cmo
+lib/frama-c/plugins/top/Variadic.cmx
+lib/frama-c/plugins/top/Variadic.cmxs
+lib/frama-c/plugins/top/Wp.cma
+lib/frama-c/plugins/top/Wp.cmx
+lib/frama-c/plugins/top/Wp.cmxa
+lib/frama-c/plugins/top/Wp.cmxs
+lib/frama-c/precise_locs.cmi
+lib/frama-c/precise_locs.cmo
+lib/frama-c/precise_locs.cmx
+lib/frama-c/precise_locs.o
${PLIST.gui}lib/frama-c/pretty_source.cmi
${PLIST.gui}lib/frama-c/pretty_source.cmo
${PLIST.gui}lib/frama-c/pretty_source.cmx
@@ -634,10 +727,11 @@ lib/frama-c/printer.cmi
lib/frama-c/printer.cmo
lib/frama-c/printer.cmx
lib/frama-c/printer.o
-lib/frama-c/printexc_common_interface.cmi
-lib/frama-c/printexc_common_interface.cmo
-lib/frama-c/printexc_common_interface.cmx
-lib/frama-c/printexc_common_interface.o
+lib/frama-c/printer_api.cmi
+lib/frama-c/printer_builder.cmi
+lib/frama-c/printer_builder.cmo
+lib/frama-c/printer_builder.cmx
+lib/frama-c/printer_builder.o
lib/frama-c/project.cmi
lib/frama-c/project.cmo
lib/frama-c/project.cmx
@@ -663,6 +757,8 @@ lib/frama-c/property_status.cmo
lib/frama-c/property_status.cmx
lib/frama-c/property_status.o
lib/frama-c/ptests_config.cmi
+lib/frama-c/ptests_config.cmx
+lib/frama-c/ptests_config.o
lib/frama-c/qstack.cmi
lib/frama-c/qstack.cmo
lib/frama-c/qstack.cmx
@@ -671,14 +767,10 @@ lib/frama-c/rangemap.cmi
lib/frama-c/rangemap.cmo
lib/frama-c/rangemap.cmx
lib/frama-c/rangemap.o
-lib/frama-c/reachingdefs.cmi
-lib/frama-c/reachingdefs.cmo
-lib/frama-c/reachingdefs.cmx
-lib/frama-c/reachingdefs.o
-lib/frama-c/rmciltmps.cmi
-lib/frama-c/rmciltmps.cmo
-lib/frama-c/rmciltmps.cmx
-lib/frama-c/rmciltmps.o
+lib/frama-c/rgmap.cmi
+lib/frama-c/rgmap.cmo
+lib/frama-c/rgmap.cmx
+lib/frama-c/rgmap.o
lib/frama-c/rmtmps.cmi
lib/frama-c/rmtmps.cmo
lib/frama-c/rmtmps.cmx
@@ -687,10 +779,6 @@ lib/frama-c/service_graph.cmi
lib/frama-c/service_graph.cmo
lib/frama-c/service_graph.cmx
lib/frama-c/service_graph.o
-lib/frama-c/setWithNearest.cmi
-lib/frama-c/setWithNearest.cmo
-lib/frama-c/setWithNearest.cmx
-lib/frama-c/setWithNearest.o
@comment lib/frama-c/shifted_Location.cmi
@comment lib/frama-c/shifted_Location.cmo
@comment lib/frama-c/shifted_Location.cmx
@@ -755,10 +843,6 @@ lib/frama-c/structural_descr.cmi
lib/frama-c/structural_descr.cmo
lib/frama-c/structural_descr.cmx
lib/frama-c/structural_descr.o
-lib/frama-c/subst.cmi
-lib/frama-c/subst.cmo
-lib/frama-c/subst.cmx
-lib/frama-c/subst.o
lib/frama-c/task.cmi
lib/frama-c/task.cmo
lib/frama-c/task.cmx
@@ -767,6 +851,10 @@ lib/frama-c/tr_offset.cmi
lib/frama-c/tr_offset.cmo
lib/frama-c/tr_offset.cmx
lib/frama-c/tr_offset.o
+lib/frama-c/transitioning.cmi
+lib/frama-c/transitioning.cmo
+lib/frama-c/transitioning.cmx
+lib/frama-c/transitioning.o
lib/frama-c/translate_lightweight.cmi
lib/frama-c/translate_lightweight.cmo
lib/frama-c/translate_lightweight.cmx
@@ -775,6 +863,14 @@ lib/frama-c/type.cmi
lib/frama-c/type.cmo
lib/frama-c/type.cmx
lib/frama-c/type.o
+lib/frama-c/typed_parameter.cmi
+lib/frama-c/typed_parameter.cmo
+lib/frama-c/typed_parameter.cmx
+lib/frama-c/typed_parameter.o
+lib/frama-c/undefined_sequence.cmi
+lib/frama-c/undefined_sequence.cmo
+lib/frama-c/undefined_sequence.cmx
+lib/frama-c/undefined_sequence.o
lib/frama-c/unicode.cmi
lib/frama-c/unicode.cmo
lib/frama-c/unicode.cmx
@@ -783,26 +879,26 @@ lib/frama-c/unmarshal.cmi
lib/frama-c/unmarshal.cmo
lib/frama-c/unmarshal.cmx
lib/frama-c/unmarshal.o
-lib/frama-c/unmarshal_nums.cmi
-lib/frama-c/unmarshal_nums.cmo
-lib/frama-c/unmarshal_nums.cmx
-lib/frama-c/unmarshal_nums.o
+lib/frama-c/unmarshal_z.cmi
+lib/frama-c/unmarshal_z.cmo
+lib/frama-c/unmarshal_z.cmx
+lib/frama-c/unmarshal_z.o
lib/frama-c/unroll_loops.cmi
lib/frama-c/unroll_loops.cmo
lib/frama-c/unroll_loops.cmx
lib/frama-c/unroll_loops.o
-lib/frama-c/usedef.cmi
-lib/frama-c/usedef.cmo
-lib/frama-c/usedef.cmx
-lib/frama-c/usedef.o
lib/frama-c/utf8_logic.cmi
lib/frama-c/utf8_logic.cmo
lib/frama-c/utf8_logic.cmx
lib/frama-c/utf8_logic.o
-lib/frama-c/value_aux.cmi
-lib/frama-c/value_aux.cmo
-lib/frama-c/value_aux.cmx
-lib/frama-c/value_aux.o
+lib/frama-c/value_types.cmi
+lib/frama-c/value_types.cmo
+lib/frama-c/value_types.cmx
+lib/frama-c/value_types.o
+lib/frama-c/vector.cmi
+lib/frama-c/vector.cmo
+lib/frama-c/vector.cmx
+lib/frama-c/vector.o
lib/frama-c/visitor.cmi
lib/frama-c/visitor.cmo
lib/frama-c/visitor.cmx
@@ -811,10 +907,14 @@ ${PLIST.gui}lib/frama-c/warning_manager.
${PLIST.gui}lib/frama-c/warning_manager.cmo
${PLIST.gui}lib/frama-c/warning_manager.cmx
${PLIST.gui}lib/frama-c/warning_manager.o
-lib/frama-c/whitetrack.cmi
-lib/frama-c/whitetrack.cmo
-lib/frama-c/whitetrack.cmx
-lib/frama-c/whitetrack.o
+lib/frama-c/wbox.cmi
+lib/frama-c/wbox.cmo
+lib/frama-c/wbox.cmx
+lib/frama-c/wbox.o
+lib/frama-c/wfile.cmi
+lib/frama-c/wfile.cmo
+lib/frama-c/wfile.cmx
+lib/frama-c/wfile.o
@comment lib/frama-c/widen.cmi
@comment lib/frama-c/widen.cmo
@comment lib/frama-c/widen.cmx
@@ -823,53 +923,111 @@ lib/frama-c/widen_type.cmi
lib/frama-c/widen_type.cmo
lib/frama-c/widen_type.cmx
lib/frama-c/widen_type.o
+lib/frama-c/widget.cmi
+lib/frama-c/widget.cmo
+lib/frama-c/widget.cmx
+lib/frama-c/widget.o
+lib/frama-c/wpalette.cmi
+lib/frama-c/wpalette.cmo
+lib/frama-c/wpalette.cmx
+lib/frama-c/wpalette.o
+lib/frama-c/wpane.cmi
+lib/frama-c/wpane.cmo
+lib/frama-c/wpane.cmx
+lib/frama-c/wpane.o
+lib/frama-c/wtable.cmi
+lib/frama-c/wtable.cmo
+lib/frama-c/wtable.cmx
+lib/frama-c/wtable.o
+lib/frama-c/wtext.cmi
+lib/frama-c/wtext.cmo
+lib/frama-c/wtext.cmx
+lib/frama-c/wtext.o
+lib/frama-c/wto.cmi
+lib/frama-c/wto.cmo
+lib/frama-c/wto.cmx
+lib/frama-c/wto.o
+lib/frama-c/wto_statement.cmi
+lib/frama-c/wto_statement.cmo
+lib/frama-c/wto_statement.cmx
+lib/frama-c/wto_statement.o
+lib/frama-c/wutil.cmi
+lib/frama-c/wutil.cmo
+lib/frama-c/wutil.cmx
+lib/frama-c/wutil.o
+lib/libeacsl-gmp.a
+lib/libeacsl-jemalloc.a
+man/man1/e-acsl-gcc.sh.1
man/man1/frama-c-gui.1
man/man1/frama-c.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.generic
share/frama-c/Makefile.kernel
-share/frama-c/Makefile.plugin
-share/frama-c/acsl.el
-share/frama-c/builtin.c
+share/frama-c/Makefile.plugin.template
+share/frama-c/autocomplete_frama-c
share/frama-c/builtin.h
@comment share/frama-c/check.png
share/frama-c/configure.ac
-share/frama-c/doc/code/docgen_ge400.ml
-share/frama-c/doc/code/docgen_lt400.ml
+share/frama-c/doc/code/docgen.ml
share/frama-c/doc/code/intro_kernel_plugin.txt
share/frama-c/doc/code/intro_plugin.txt
share/frama-c/doc/code/intro_plugin_default.txt
share/frama-c/doc/code/style.css
share/frama-c/doc/code/toc_head.htm
share/frama-c/doc/code/toc_tail.htm
+share/frama-c/e-acsl/bittree_model/e_acsl_bittree.h
+share/frama-c/e-acsl/bittree_model/e_acsl_bittree_api.h
+share/frama-c/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+share/frama-c/e-acsl/e_acsl.h
+share/frama-c/e-acsl/e_acsl_assert.h
+share/frama-c/e-acsl/e_acsl_bits.h
+share/frama-c/e-acsl/e_acsl_debug.h
+share/frama-c/e-acsl/e_acsl_gmp.h
+share/frama-c/e-acsl/e_acsl_malloc.h
+share/frama-c/e-acsl/e_acsl_mmodel.c
+share/frama-c/e-acsl/e_acsl_mmodel_api.h
+share/frama-c/e-acsl/e_acsl_printf.h
+share/frama-c/e-acsl/e_acsl_safe_locations.h
+share/frama-c/e-acsl/e_acsl_shexec.h
+share/frama-c/e-acsl/e_acsl_string.h
+share/frama-c/e-acsl/e_acsl_syscall.h
+share/frama-c/e-acsl/e_acsl_trace.h
+share/frama-c/e-acsl/glibc/memcmp.c
+share/frama-c/e-acsl/glibc/memcopy.h
+share/frama-c/e-acsl/glibc/memcpy.c
+share/frama-c/e-acsl/glibc/memmove.c
+share/frama-c/e-acsl/glibc/memset.c
+share/frama-c/e-acsl/glibc/pagecopy.h
+share/frama-c/e-acsl/glibc/strcmp.c
+share/frama-c/e-acsl/glibc/strlen.c
+share/frama-c/e-acsl/glibc/strncmp.c
+share/frama-c/e-acsl/glibc/wordcopy.c
+share/frama-c/e-acsl/segment_model/e_acsl_segment_mmodel.c
+share/frama-c/e-acsl/segment_model/e_acsl_segment_tracking.h
+share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h
+share/frama-c/emacs/acsl.el
+share/frama-c/emacs/frama-c-dev.el
+share/frama-c/emacs/frama-c-init.el
+share/frama-c/emacs/frama-c-recommended.el
@comment share/frama-c/failed.png
-share/frama-c/feedback/considered_valid.png
-share/frama-c/feedback/inconsistent.png
-share/frama-c/feedback/invalid_but_dead.png
-share/frama-c/feedback/invalid_under_hyp.png
-share/frama-c/feedback/never_tried.png
-share/frama-c/feedback/surely_invalid.png
-share/frama-c/feedback/surely_valid.png
-share/frama-c/feedback/unknown.png
-share/frama-c/feedback/unknown_but_dead.png
-share/frama-c/feedback/valid_but_dead.png
-share/frama-c/feedback/valid_under_hyp.png
-share/frama-c/fluctuat.h
-share/frama-c/frama-c.gif
share/frama-c/frama-c.ico
+share/frama-c/frama-c.png
share/frama-c/frama-c.rc
@comment share/frama-c/left.png
share/frama-c/libc.c
-share/frama-c/libc.h
share/frama-c/libc/__fc_builtin.c
share/frama-c/libc/__fc_builtin.h
share/frama-c/libc/__fc_builtin_for_normalization.i
share/frama-c/libc/__fc_define_blkcnt_t.h
share/frama-c/libc/__fc_define_blksize_t.h
share/frama-c/libc/__fc_define_dev_t.h
+share/frama-c/libc/__fc_define_eof.h
share/frama-c/libc/__fc_define_fd_set_t.h
+share/frama-c/libc/__fc_define_file.h
+share/frama-c/libc/__fc_define_fpos_t.h
share/frama-c/libc/__fc_define_id_t.h
share/frama-c/libc/__fc_define_ino_t.h
share/frama-c/libc/__fc_define_intptr_t.h
@@ -879,76 +1037,77 @@ share/frama-c/libc/__fc_define_nlink_t.h
share/frama-c/libc/__fc_define_null.h
share/frama-c/libc/__fc_define_off_t.h
share/frama-c/libc/__fc_define_pid_t.h
-share/frama-c/libc/__fc_define_restrict.h
share/frama-c/libc/__fc_define_sa_family_t.h
share/frama-c/libc/__fc_define_seek_macros.h
share/frama-c/libc/__fc_define_sigset_t.h
share/frama-c/libc/__fc_define_size_t.h
share/frama-c/libc/__fc_define_sockaddr.h
share/frama-c/libc/__fc_define_ssize_t.h
+share/frama-c/libc/__fc_define_stat.h
share/frama-c/libc/__fc_define_suseconds_t.h
share/frama-c/libc/__fc_define_time_t.h
share/frama-c/libc/__fc_define_timespec.h
share/frama-c/libc/__fc_define_uid_and_gid.h
share/frama-c/libc/__fc_define_useconds_t.h
share/frama-c/libc/__fc_define_wchar_t.h
+share/frama-c/libc/__fc_define_wint_t.h
share/frama-c/libc/__fc_machdep.h
+share/frama-c/libc/__fc_machdep_linux_gcc_shared.h
+share/frama-c/libc/__fc_select.h
share/frama-c/libc/__fc_string_axiomatic.h
-share/frama-c/libc/arpa/inet.c
share/frama-c/libc/arpa/inet.h
share/frama-c/libc/assert.c
share/frama-c/libc/assert.h
-share/frama-c/libc/complex.c
+share/frama-c/libc/byteswap.h
share/frama-c/libc/complex.h
share/frama-c/libc/ctype.c
share/frama-c/libc/ctype.h
-share/frama-c/libc/dirent.c
share/frama-c/libc/dirent.h
+share/frama-c/libc/dlfcn.h
+share/frama-c/libc/endian.h
share/frama-c/libc/errno.c
share/frama-c/libc/errno.h
-share/frama-c/libc/fc_posix_runtime.c
share/frama-c/libc/fc_runtime.c
-share/frama-c/libc/fcntl.c
share/frama-c/libc/fcntl.h
-share/frama-c/libc/fenv.c
+share/frama-c/libc/features.h
share/frama-c/libc/fenv.h
-share/frama-c/libc/float.c
share/frama-c/libc/float.h
-share/frama-c/libc/inttypes.c
-share/frama-c/libc/inttypes.h
-share/frama-c/libc/iconv.c
+share/frama-c/libc/getopt.c
+share/frama-c/libc/getopt.h
+share/frama-c/libc/glob.h
+share/frama-c/libc/grp.h
share/frama-c/libc/iconv.h
-share/frama-c/libc/ifaddrs.c
share/frama-c/libc/ifaddrs.h
-share/frama-c/libc/iso646.c
+share/frama-c/libc/inttypes.c
+share/frama-c/libc/inttypes.h
share/frama-c/libc/iso646.h
-share/frama-c/libc/limits.c
+share/frama-c/libc/libgen.h
+share/frama-c/libc/libintl.h
share/frama-c/libc/limits.h
-share/frama-c/libc/linux/fs.c
share/frama-c/libc/linux/fs.h
+share/frama-c/libc/linux/if_addr.h
+share/frama-c/libc/linux/if_netlink.h
+share/frama-c/libc/linux/netlink.h
+share/frama-c/libc/linux/rtnetlink.h
share/frama-c/libc/locale.c
share/frama-c/libc/locale.h
share/frama-c/libc/math.c
share/frama-c/libc/math.h
-share/frama-c/libc/net/if.c
share/frama-c/libc/net/if.h
-share/frama-c/libc/netinet/in.c
+share/frama-c/libc/netdb.h
share/frama-c/libc/netinet/in.h
-share/frama-c/libc/nl_types.c
+share/frama-c/libc/netinet/in_systm.h
+share/frama-c/libc/netinet/ip.h
+share/frama-c/libc/netinet/ip_icmp.h
+share/frama-c/libc/netinet/tcp.h
share/frama-c/libc/nl_types.h
-share/frama-c/libc/pwd.c
share/frama-c/libc/pwd.h
-share/frama-c/libc/setjmp.c
+share/frama-c/libc/regex.h
share/frama-c/libc/setjmp.h
-share/frama-c/libc/signal.c
share/frama-c/libc/signal.h
-share/frama-c/libc/stdarg.c
share/frama-c/libc/stdarg.h
-share/frama-c/libc/stdbool.c
share/frama-c/libc/stdbool.h
-share/frama-c/libc/stddef.c
share/frama-c/libc/stddef.h
-share/frama-c/libc/stdint.c
share/frama-c/libc/stdint.h
share/frama-c/libc/stdio.c
share/frama-c/libc/stdio.h
@@ -956,85 +1115,145 @@ share/frama-c/libc/stdlib.c
share/frama-c/libc/stdlib.h
share/frama-c/libc/string.c
share/frama-c/libc/string.h
-share/frama-c/libc/strings.c
share/frama-c/libc/strings.h
-share/frama-c/libc/sys/ioctl.c
share/frama-c/libc/sys/ioctl.h
-share/frama-c/libc/sys/param.c
share/frama-c/libc/sys/param.h
-share/frama-c/libc/sys/resource.c
share/frama-c/libc/sys/resource.h
-share/frama-c/libc/sys/select.c
share/frama-c/libc/sys/select.h
-share/frama-c/libc/sys/socket.c
share/frama-c/libc/sys/socket.h
-share/frama-c/libc/sys/stat.c
share/frama-c/libc/sys/stat.h
-share/frama-c/libc/sys/time.c
+share/frama-c/libc/sys/sysctl.h
share/frama-c/libc/sys/time.h
-share/frama-c/libc/sys/types.c
+share/frama-c/libc/sys/times.h
share/frama-c/libc/sys/types.h
-share/frama-c/libc/sys/uio.c
share/frama-c/libc/sys/uio.h
-share/frama-c/libc/sys/un.c
share/frama-c/libc/sys/un.h
-share/frama-c/libc/sys/wait.c
share/frama-c/libc/sys/wait.h
-share/frama-c/libc/syslog.c
share/frama-c/libc/syslog.h
-share/frama-c/libc/termios.c
share/frama-c/libc/termios.h
-share/frama-c/libc/test.c
-share/frama-c/libc/tgmath.c
share/frama-c/libc/tgmath.h
-share/frama-c/libc/time.c
share/frama-c/libc/time.h
-share/frama-c/libc/uchar.c
share/frama-c/libc/uchar.h
-share/frama-c/libc/unistd.c
share/frama-c/libc/unistd.h
share/frama-c/libc/wchar.c
share/frama-c/libc/wchar.h
-share/frama-c/libc/wctype.c
share/frama-c/libc/wctype.h
-share/frama-c/machine.h
-share/frama-c/malloc.c
-share/frama-c/manuals/acsl-implementation.pdf
-share/frama-c/manuals/acsl.pdf
-share/frama-c/manuals/aorai-manual.pdf
-@comment share/frama-c/manuals/jessie-tutorial.pdf
-share/frama-c/manuals/metrics-manual.pdf
-share/frama-c/manuals/plugin-development-guide.pdf
-share/frama-c/manuals/rte-manual.pdf
-share/frama-c/manuals/user-manual.pdf
-share/frama-c/manuals/value-analysis.pdf
-share/frama-c/manuals/wp-manual.pdf
-share/frama-c/manuals/wp-tutorial.pdf
-share/frama-c/math.c
-share/frama-c/math.h
+share/frama-c/machdep.c
@comment share/frama-c/maybe.png
@comment share/frama-c/right.png
+share/frama-c/switch-off.png
+share/frama-c/switch-on.png
+share/frama-c/theme/colorblind/considered_valid.png
+share/frama-c/theme/colorblind/inconsistent.png
+share/frama-c/theme/colorblind/invalid_but_dead.png
+share/frama-c/theme/colorblind/invalid_under_hyp.png
+share/frama-c/theme/colorblind/never_tried.png
+share/frama-c/theme/colorblind/surely_invalid.png
+share/frama-c/theme/colorblind/surely_valid.png
+share/frama-c/theme/colorblind/unknown.png
+share/frama-c/theme/colorblind/unknown_but_dead.png
+share/frama-c/theme/colorblind/valid_but_dead.png
+share/frama-c/theme/colorblind/valid_under_hyp.png
+share/frama-c/theme/default/considered_valid.png
+share/frama-c/theme/default/inconsistent.png
+share/frama-c/theme/default/invalid_but_dead.png
+share/frama-c/theme/default/invalid_under_hyp.png
+share/frama-c/theme/default/never_tried.png
+share/frama-c/theme/default/surely_invalid.png
+share/frama-c/theme/default/surely_valid.png
+share/frama-c/theme/default/unknown.png
+share/frama-c/theme/default/unknown_but_dead.png
+share/frama-c/theme/default/valid_but_dead.png
+share/frama-c/theme/default/valid_under_hyp.png
share/frama-c/unmark.png
-share/frama-c/wp/Cfloat.v
-share/frama-c/wp/Cint.v
-share/frama-c/wp/Cmath.v
-share/frama-c/wp/Memory.v
-share/frama-c/wp/Qedlib.v
-share/frama-c/wp/Vset.v
-share/frama-c/wp/cfloat.mlw
-share/frama-c/wp/cint.mlw
-share/frama-c/wp/cmath.mlw
-share/frama-c/wp/hoare_ergo.why
-share/frama-c/wp/hoare_model.v
-share/frama-c/wp/hoare_model.why
-share/frama-c/wp/memory.mlw
-share/frama-c/wp/qed.mlw
-share/frama-c/wp/runtime_ergo.why
-share/frama-c/wp/runtime_model.v
-share/frama-c/wp/runtime_model.why
-share/frama-c/wp/store_ergo.why
-share/frama-c/wp/store_model.v
-share/frama-c/wp/store_model.why
-share/frama-c/wp/vset.mlw
-share/frama-c/wp/wp.v
+share/frama-c/wp/coqwp/Bits.v
+${PLIST.coq}share/frama-c/wp/coqwp/Bits.vo
+share/frama-c/wp/coqwp/BuiltIn.v
+${PLIST.coq}share/frama-c/wp/coqwp/BuiltIn.vo
+share/frama-c/wp/coqwp/Cbits.v
+${PLIST.coq}share/frama-c/wp/coqwp/Cbits.vo
+share/frama-c/wp/coqwp/Cfloat.v
+${PLIST.coq}share/frama-c/wp/coqwp/Cfloat.vo
+share/frama-c/wp/coqwp/Cint.v
+${PLIST.coq}share/frama-c/wp/coqwp/Cint.vo
+share/frama-c/wp/coqwp/Cmath.v
+${PLIST.coq}share/frama-c/wp/coqwp/Cmath.vo
+share/frama-c/wp/coqwp/Memory.v
+${PLIST.coq}share/frama-c/wp/coqwp/Memory.vo
+share/frama-c/wp/coqwp/Qed.v
+${PLIST.coq}share/frama-c/wp/coqwp/Qed.vo
+share/frama-c/wp/coqwp/Qedlib.v
+${PLIST.coq}share/frama-c/wp/coqwp/Qedlib.vo
+share/frama-c/wp/coqwp/Vlist.v
+${PLIST.coq}share/frama-c/wp/coqwp/Vlist.vo
+share/frama-c/wp/coqwp/Vset.v
+${PLIST.coq}share/frama-c/wp/coqwp/Vset.vo
+share/frama-c/wp/coqwp/Zbits.v
+${PLIST.coq}share/frama-c/wp/coqwp/Zbits.vo
+share/frama-c/wp/coqwp/bool/Bool.v
+${PLIST.coq}share/frama-c/wp/coqwp/bool/Bool.vo
+share/frama-c/wp/coqwp/int/Abs.v
+${PLIST.coq}share/frama-c/wp/coqwp/int/Abs.vo
+share/frama-c/wp/coqwp/int/ComputerDivision.v
+${PLIST.coq}share/frama-c/wp/coqwp/int/ComputerDivision.vo
+share/frama-c/wp/coqwp/int/Int.v
+${PLIST.coq}share/frama-c/wp/coqwp/int/Int.vo
+share/frama-c/wp/coqwp/int/MinMax.v
+${PLIST.coq}share/frama-c/wp/coqwp/int/MinMax.vo
+share/frama-c/wp/coqwp/map/Map.v
+${PLIST.coq}share/frama-c/wp/coqwp/map/Map.vo
+share/frama-c/wp/coqwp/real/Abs.v
+${PLIST.coq}share/frama-c/wp/coqwp/real/Abs.vo
+share/frama-c/wp/coqwp/real/FromInt.v
+${PLIST.coq}share/frama-c/wp/coqwp/real/FromInt.vo
+share/frama-c/wp/coqwp/real/MinMax.v
+${PLIST.coq}share/frama-c/wp/coqwp/real/MinMax.vo
+share/frama-c/wp/coqwp/real/Real.v
+${PLIST.coq}share/frama-c/wp/coqwp/real/Real.vo
+share/frama-c/wp/coqwp/real/RealInfix.v
+${PLIST.coq}share/frama-c/wp/coqwp/real/RealInfix.vo
+share/frama-c/wp/coqwp/real/Square.v
+${PLIST.coq}share/frama-c/wp/coqwp/real/Square.vo
+share/frama-c/wp/ergo/Cbits.mlw
+share/frama-c/wp/ergo/Cfloat.mlw
+share/frama-c/wp/ergo/Cint.mlw
+share/frama-c/wp/ergo/Cmath.mlw
+share/frama-c/wp/ergo/Memory.mlw
+share/frama-c/wp/ergo/Qed.mlw
+share/frama-c/wp/ergo/Vlist.mlw
+share/frama-c/wp/ergo/Vset.mlw
+share/frama-c/wp/ergo/bool.Bool.mlw
+share/frama-c/wp/ergo/int.Abs.mlw
+share/frama-c/wp/ergo/int.ComputerDivision.mlw
+share/frama-c/wp/ergo/int.Int.mlw
+share/frama-c/wp/ergo/int.MinMax.mlw
+share/frama-c/wp/ergo/map.Map.mlw
+share/frama-c/wp/ergo/real.Abs.mlw
+share/frama-c/wp/ergo/real.FromInt.mlw
+share/frama-c/wp/ergo/real.MinMax.mlw
+share/frama-c/wp/ergo/real.Real.mlw
+share/frama-c/wp/ergo/real.RealInfix.mlw
+share/frama-c/wp/ergo/real.Square.mlw
+share/frama-c/wp/why3/Bits.v
+share/frama-c/wp/why3/Cbits.v
+share/frama-c/wp/why3/Cbits.why
+share/frama-c/wp/why3/Cfloat.v
+share/frama-c/wp/why3/Cfloat.why
+share/frama-c/wp/why3/Cint.v
+share/frama-c/wp/why3/Cint.why
+share/frama-c/wp/why3/Cmath.v
+share/frama-c/wp/why3/Cmath.why
+share/frama-c/wp/why3/Memory.v
+share/frama-c/wp/why3/Memory.why
+share/frama-c/wp/why3/Qed.v
+share/frama-c/wp/why3/Qed.why
+share/frama-c/wp/why3/Qedlib.v
+share/frama-c/wp/why3/Vlist.v
+share/frama-c/wp/why3/Vlist.why
+share/frama-c/wp/why3/Vset.v
+share/frama-c/wp/why3/Vset.why
+share/frama-c/wp/why3/Zbits.v
+share/frama-c/wp/why3/coq.drv
+share/frama-c/wp/why3/why3.conf
+share/frama-c/wp/wp.driver
@pkgdir lib/frama-c/plugins/gui
Index: pkgsrc/devel/frama-c/distinfo
diff -u pkgsrc/devel/frama-c/distinfo:1.6 pkgsrc/devel/frama-c/distinfo:1.7
--- pkgsrc/devel/frama-c/distinfo:1.6 Tue Nov 3 03:27:26 2015
+++ pkgsrc/devel/frama-c/distinfo Tue Sep 5 07:30:00 2017
@@ -1,7 +1,14 @@
-$NetBSD: distinfo,v 1.6 2015/11/03 03:27:26 agc Exp $
+$NetBSD: distinfo,v 1.7 2017/09/05 07:30:00 dholland Exp $
-SHA1 (frama-c-Oxygen-20120901.tar.gz) = 65aef0a88b788d11a6b5061dc08741492859de40
-RMD160 (frama-c-Oxygen-20120901.tar.gz) = 76daf11770a52b1b1bc59ca9c576208ac08755a8
-SHA512 (frama-c-Oxygen-20120901.tar.gz) = fcf96dd2c0e50c4f125050b677f55d960d3a78d2d827cbb6f9ddd98892162cb1181053202ce46f74911b29ad895489d51939a2bb52dafed440ee2abcbde41224
-Size (frama-c-Oxygen-20120901.tar.gz) = 10815011 bytes
-SHA1 (patch-configure) = c7e895c967199433c9d55d99347ec14cad9b41ab
+SHA1 (frama-c-Phosphorus-20170501.tar.gz) = d9372127ba80636cc1c692a141a7a02dee8325da
+RMD160 (frama-c-Phosphorus-20170501.tar.gz) = 24a5b8578491d3c15aa539da69062803d0c6d137
+SHA512 (frama-c-Phosphorus-20170501.tar.gz) = b3b73932378cba7be8ac0cbb1f7311e8f60dde68cad55c10659ffa40e76ab3f106d554e245ccd90ffb5307b9a42b6ce51154a5b9c006687b8c5808c77ca4c2f3
+Size (frama-c-Phosphorus-20170501.tar.gz) = 7431131 bytes
+SHA1 (patch-Makefile) = d9a23653196d4586c3cca87091518aea6791ddcc
+SHA1 (patch-configure) = a415684ab5ecb4fed276dede90439fa8ba6a09ed
+SHA1 (patch-share_Makefile.common) = f5230aee768e6af4c7458d96f1f210172daa9bb2
+SHA1 (patch-src_libraries_utils_c__bindings.c) = b37db1c51e9082e4a328a6a7189f57db3f12d624
+SHA1 (patch-src_plugins_e-acsl_Makefile) = 02542a247a7f4b266c7e9139c4ee555dda5fd1bb
+SHA1 (patch-src_plugins_wp_configure) = 6f0fb756d2460b6abf27313d367672e293a8d9e7
+SHA1 (patch-src_plugins_wp_configure.ac) = 3b15ff7b551da79ad1580b134258631f1527bc42
+SHA1 (patch-src_plugins_wp_share_coqwp_Zbits.v) = 26fac23dc015087b7126e40a47d566eb49a24293
Index: pkgsrc/devel/frama-c/options.mk
diff -u pkgsrc/devel/frama-c/options.mk:1.3 pkgsrc/devel/frama-c/options.mk:1.4
--- pkgsrc/devel/frama-c/options.mk:1.3 Sun Dec 25 15:52:12 2011
+++ pkgsrc/devel/frama-c/options.mk Tue Sep 5 07:30:00 2017
@@ -1,17 +1,25 @@
-# $NetBSD: options.mk,v 1.3 2011/12/25 15:52:12 asau Exp $
+# $NetBSD: options.mk,v 1.4 2017/09/05 07:30:00 dholland Exp $
PKG_OPTIONS_VAR= PKG_OPTIONS.frama-c
-PKG_SUPPORTED_OPTIONS= gui
-PKG_SUGGESTED_OPTIONS= gui
+PKG_SUPPORTED_OPTIONS= gui coq
+PKG_SUGGESTED_OPTIONS= gui coq
-PLIST_VARS= gui
+PLIST_VARS= gui coq
.include "../../mk/bsd.options.mk"
.if !empty(PKG_OPTIONS:Mgui)
PLIST.gui= yes
-.include "../../x11/gtksourceview2/buildlink3.mk"
+.include "../../x11/ocaml-lablgtk/buildlink3.mk"
.else
CONFIGURE_ARGS+= --enable-gui=no
.endif
+
+.if !empty(PKG_OPTIONS:Mcoq)
+PLIST.coq= yes
+
+DEPENDS+= coq>=8.6:../../lang/coq
+.else
+CONFIGURE_ARGS+= --enable-wp-coq=no
+.endif
Index: pkgsrc/devel/frama-c/patches/patch-configure
diff -u pkgsrc/devel/frama-c/patches/patch-configure:1.1 pkgsrc/devel/frama-c/patches/patch-configure:1.2
--- pkgsrc/devel/frama-c/patches/patch-configure:1.1 Fri Nov 15 14:10:29 2013
+++ pkgsrc/devel/frama-c/patches/patch-configure Tue Sep 5 07:30:00 2017
@@ -1,15 +1,15 @@
-$NetBSD: patch-configure,v 1.1 2013/11/15 14:10:29 wiz Exp $
+$NetBSD: patch-configure,v 1.2 2017/09/05 07:30:00 dholland Exp $
-Fix GNU make version comparison logic.
+Recognize more recent coq.
---- configure.orig 2013-11-15 14:08:17.000000000 +0000
+--- configure~ 2017-06-01 08:02:19.000000000 +0000
+++ configure
-@@ -2617,7 +2617,7 @@ MAKE_DISTRIB=`$MAKE -v | sed -n -e 's/\(
- MAKE_MAJOR=`$MAKE -v | sed -n -f bin/sed_get_make_major `
- MAKE_MINOR=`$MAKE -v | sed -n -f bin/sed_get_make_minor `
- echo $ECHO_N "make version is $MAKE_DISTRIB Make $MAKE_MAJOR.$MAKE_MINOR: $ECHO_C"
--if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MINOR" -lt 81;
-+if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MAJOR" -eq 3 -a "$MAKE_MINOR" -lt 81;
- then
- echo "${ECHO_T}"
- as_fn_error $? "unsupported version; GNU Make version 3.81
+@@ -11308,7 +11308,7 @@ fi
+ if test "$COQC" = "yes" ; then
+ COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([^ ]*\) .*$|\1|p' `
+ case $COQVERSION in
+- 8.4pl6|8.5*|trunk)
++ 8.4pl6|8.5*|8.6*|trunk)
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: coqc version $COQVERSION found" >&5
+ $as_echo "coqc version $COQVERSION found" >&6; }
+ ;;
Added files:
Index: pkgsrc/devel/frama-c/patches/patch-Makefile
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-Makefile:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-Makefile Tue Sep 5 07:30:00 2017
@@ -0,0 +1,85 @@
+$NetBSD: patch-Makefile,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+Don't install nonexecutables with execute permission.
+
+--- Makefile.orig 2017-06-01 08:02:11.000000000 +0000
++++ Makefile
+@@ -1527,30 +1527,30 @@ install:: install-lib
+ $(MKDIR) $(FRAMAC_DATADIR)/libc/net
+ $(MKDIR) $(FRAMAC_DATADIR)/libc/arpa
+ $(PRINT_INSTALL) shared files
+- $(CP) \
++ $(CPNX) \
+ $(wildcard share/*.c share/*.h) \
+ share/Makefile.dynamic share/Makefile.plugin.template share/Makefile.kernel \
+ share/Makefile.config share/Makefile.common share/Makefile.generic \
+ share/configure.ac share/autocomplete_frama-c \
+ $(FRAMAC_DATADIR)
+ $(MKDIR) $(FRAMAC_DATADIR)/emacs
+- $(CP) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs
+- $(CP) share/frama-c.rc $(ICONS) $(FRAMAC_DATADIR)
+- $(CP) $(FEEDBACK_ICONS_DEFAULT) $(FRAMAC_DATADIR)/theme/default
+- $(CP) $(FEEDBACK_ICONS_COLORBLIND) $(FRAMAC_DATADIR)/theme/colorblind
++ $(CPNX) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs
++ $(CPNX) share/frama-c.rc $(ICONS) $(FRAMAC_DATADIR)
++ $(CPNX) $(FEEDBACK_ICONS_DEFAULT) $(FRAMAC_DATADIR)/theme/default
++ $(CPNX) $(FEEDBACK_ICONS_COLORBLIND) $(FRAMAC_DATADIR)/theme/colorblind
+ if [ -d $(EMACS_DATADIR) ]; then \
+- $(CP) $(wildcard share/emacs/*.el) $(EMACS_DATADIR); \
++ $(CPNX) $(wildcard share/emacs/*.el) $(EMACS_DATADIR); \
+ fi
+- $(CP) share/Makefile.dynamic_config.external \
++ $(CPNX) share/Makefile.dynamic_config.external \
+ $(FRAMAC_DATADIR)/Makefile.dynamic_config
+ $(PRINT_INSTALL) C standard library
+- $(CP) $(wildcard share/libc/*.c share/libc/*.i share/libc/*.h) \
++ $(CPNX) $(wildcard share/libc/*.c share/libc/*.i share/libc/*.h) \
+ $(FRAMAC_DATADIR)/libc
+- $(CP) share/libc/sys/*.[ch] $(FRAMAC_DATADIR)/libc/sys
+- $(CP) share/libc/arpa/*.[ch] $(FRAMAC_DATADIR)/libc/arpa
+- $(CP) share/libc/net/*.[ch] $(FRAMAC_DATADIR)/libc/net
+- $(CP) share/libc/netinet/*.[ch] $(FRAMAC_DATADIR)/libc/netinet
+- $(CP) share/libc/linux/*.[ch] $(FRAMAC_DATADIR)/libc/linux
++ $(CPNX) share/libc/sys/*.[ch] $(FRAMAC_DATADIR)/libc/sys
++ $(CPNX) share/libc/arpa/*.[ch] $(FRAMAC_DATADIR)/libc/arpa
++ $(CPNX) share/libc/net/*.[ch] $(FRAMAC_DATADIR)/libc/net
++ $(CPNX) share/libc/netinet/*.[ch] $(FRAMAC_DATADIR)/libc/netinet
++ $(CPNX) share/libc/linux/*.[ch] $(FRAMAC_DATADIR)/libc/linux
+ $(PRINT_INSTALL) binaries
+ $(CP) bin/toplevel.$(OCAMLBEST) $(BINDIR)/frama-c$(EXE)
+ $(CP) bin/toplevel.byte$(EXE) $(BINDIR)/frama-c.byte$(EXE)
+@@ -1569,27 +1569,27 @@ install:: install-lib
+ $(CP) bin/frama-c-config$(EXE) $(BINDIR); \
+ fi
+ $(PRINT_INSTALL) config files
+- $(CP) $(addprefix ptests/,$(PTESTS_FILES)) $(FRAMAC_LIBDIR)
++ $(CPNX) $(addprefix ptests/,$(PTESTS_FILES)) $(FRAMAC_LIBDIR)
+ $(PRINT_INSTALL) API documentation
+ $(MKDIR) $(FRAMAC_DATADIR)/doc/code
+- $(CP) $(wildcard $(DOC_GEN_FILES)) $(FRAMAC_DATADIR)/doc/code
++ $(CPNX) $(wildcard $(DOC_GEN_FILES)) $(FRAMAC_DATADIR)/doc/code
+ $(PRINT_INSTALL) dynamic plug-ins
+ if [ -d "$(FRAMAC_PLUGIN)" -a "$(PLUGIN_DYN_EXISTS)" = "yes" ]; then \
+- $(CP) $(PLUGIN_DYN_CMI_LIST) $(PLUGIN_META_LIST) \
++ $(CPNX) $(PLUGIN_DYN_CMI_LIST) $(PLUGIN_META_LIST) \
+ $(FRAMAC_PLUGINDIR); \
+- $(CP) $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
++ $(CPNX) $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
+ $(FRAMAC_PLUGINDIR)/top; \
+ fi
+ $(PRINT_INSTALL) dynamic gui plug-ins
+ if [ -d "$(FRAMAC_PLUGIN_GUI)" -a "$(PLUGIN_DYN_GUI_EXISTS)" = "yes" ]; \
+ then \
+- $(CP) $(patsubst %.cma,%.cmi,$(PLUGIN_DYN_GUI_CMO_LIST:.cmo=.cmi)) \
++ $(CPNX) $(patsubst %.cma,%.cmi,$(PLUGIN_DYN_GUI_CMO_LIST:.cmo=.cmi)) \
+ $(PLUGIN_DYN_GUI_CMO_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \
+ $(FRAMAC_PLUGINDIR)/gui; \
+ fi
+ $(PRINT_INSTALL) man pages
+- $(CP) man/frama-c.1 $(MANDIR)/man1/frama-c.1
+- $(CP) man/frama-c.1 $(MANDIR)/man1/frama-c-gui.1
++ $(CPNX) man/frama-c.1 $(MANDIR)/man1/frama-c.1
++ $(CPNX) man/frama-c.1 $(MANDIR)/man1/frama-c-gui.1
+
+ .PHONY: uninstall
+ uninstall::
Index: pkgsrc/devel/frama-c/patches/patch-share_Makefile.common
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-share_Makefile.common:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-share_Makefile.common Tue Sep 5 07:30:00 2017
@@ -0,0 +1,14 @@
+$NetBSD: patch-share_Makefile.common,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+Don't install nonexecutables with execute permission.
+
+--- share/Makefile.common~ 2017-06-01 08:02:11.000000000 +0000
++++ share/Makefile.common
+@@ -165,6 +165,7 @@ CHMOD_RW= sh -c \
+ if test -e $$f; then chmod u+w $$f; fi \
+ done' chmod_rw
+ CP = install
++CPNX = install -m 644
+ CP_IF_DIFF = sh -c \
+ 'if cmp -s $$1 $$2; \
+ then touch -r $$2 $$1; \
Index: pkgsrc/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c Tue Sep 5 07:30:00 2017
@@ -0,0 +1,24 @@
+$NetBSD: patch-src_libraries_utils_c__bindings.c,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+sync ifdefs with reality
+
+--- src/libraries/utils/c_bindings.c~ 2017-06-01 08:02:15.000000000 +0000
++++ src/libraries/utils/c_bindings.c
+@@ -35,7 +35,7 @@
+ #include <unistd.h>
+
+ // Some BSD flavors do not implement all of C99
+-#if defined(__OpenBSD__) || defined(__NetBSD__)
++#if defined(__OpenBSD__)
+ # include <ieeefp.h>
+ # define FE_DOWNWARD FP_RM
+ # define FE_UPWARD FP_RP
+@@ -218,7 +218,7 @@ value single_precision_of_string(value s
+ value terminate_process(value v)
+ {
+ long pid = Long_val(v);
+-#if _POSIX_C_SOURCE >= 1 || _XOPEN_SOURCE || _POSIX_SOURCE || __ENVIRONMENT_MAC_OS_X_VERSION_MIN_REQUIRED__
++#if _POSIX_C_SOURCE >= 1 || _XOPEN_SOURCE || _POSIX_SOURCE || __ENVIRONMENT_MAC_OS_X_VERSION_MIN_REQUIRED__ || defined(__NetBSD__) || defined(__FreeBSD__) || defined(__OpenBSD__) ||
defined(__DragonFly__) || defined (__Bitrig__)
+ kill(pid,9);
+ #else
+ #ifdef _WIN32
Index: pkgsrc/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile Tue Sep 5 07:30:00 2017
@@ -0,0 +1,64 @@
+$NetBSD: patch-src_plugins_e-acsl_Makefile,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+Don't install nonexecutables with execute permission.
+
+--- src/plugins/e-acsl/Makefile~ 2017-09-05 07:10:24.721100926 +0000
++++ src/plugins/e-acsl/Makefile
+@@ -157,7 +157,7 @@ EACSL_JEMALLOC_LIB = $(EACSL_LIBDIR)/$(E
+ $(EACSL_JEMALLOC_LIB):
+ cd $(EACSL_JEMALLOC_DIR) && $(MAKE) $(MAKEOPTS)
+ $(MKDIR) $(EACSL_LIBDIR)
+- $(CP) $(EACSL_JEMALLOC_DIR)/lib/libjemalloc.a $@
++ $(CPNX) $(EACSL_JEMALLOC_DIR)/lib/libjemalloc.a $@
+
+ EACSL_GMP_DIR := $(EACSL_PLUGIN_DIR)/contrib/libgmp
+ EACSL_GMP_LIBNAME = libeacsl-gmp.a
+@@ -187,7 +187,7 @@ else
+ $(EACSL_GMP_LIB):
+ cd $(EACSL_GMP_DIR) && $(MAKE) $(MAKEOPTS)
+ $(MKDIR) $(EACSL_LIBDIR)
+- $(CP) $(EACSL_GMP_DIR)/.libs/libgmp.a $@
++ $(CPNX) $(EACSL_GMP_DIR)/.libs/libgmp.a $@
+ endif
+
+ all:: $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
+@@ -367,32 +367,32 @@ MANUALS=$(wildcard $(E_ACSL_DIR)/doc/man
+ install::
+ $(PRINT_INSTALL) E-ACSL share files
+ $(MKDIR) $(FRAMAC_DATADIR)/e-acsl
+- $(CP) $(E_ACSL_DIR)/share/e-acsl/*.[ch] $(FRAMAC_DATADIR)/e-acsl
++ $(CPNX) $(E_ACSL_DIR)/share/e-acsl/*.[ch] $(FRAMAC_DATADIR)/e-acsl
+ $(MKDIR) $(FRAMAC_DATADIR)/e-acsl/bittree_model \
+ $(FRAMAC_DATADIR)/e-acsl/segment_model \
+ $(FRAMAC_DATADIR)/e-acsl/glibc
+- $(CP) $(E_ACSL_DIR)/share/e-acsl/bittree_model/* \
++ $(CPNX) $(E_ACSL_DIR)/share/e-acsl/bittree_model/* \
+ $(FRAMAC_DATADIR)/e-acsl/bittree_model
+- $(CP) $(E_ACSL_DIR)/share/e-acsl/segment_model/* \
++ $(CPNX) $(E_ACSL_DIR)/share/e-acsl/segment_model/* \
+ $(FRAMAC_DATADIR)/e-acsl/segment_model
+- $(CP) $(E_ACSL_DIR)/share/e-acsl/glibc/* \
++ $(CPNX) $(E_ACSL_DIR)/share/e-acsl/glibc/* \
+ $(FRAMAC_DATADIR)/e-acsl/glibc
+ # manuals are not present in standard distribution.
+ # Don't fail because of that.
+ ifneq ("$(MANUALS)","")
+ $(PRINT_INSTALL) E-ACSL manuals
+ $(MKDIR) $(FRAMAC_DATADIR)/manuals
+- $(CP) $(MANUALS) $(FRAMAC_DATADIR)/manuals;
++ $(CPNX) $(MANUALS) $(FRAMAC_DATADIR)/manuals;
+ endif
+ $(PRINT_INSTALL) E-ACSL libraries
+ $(MKDIR) $(LIBDIR)
+- $(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR)
++ $(CPNX) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR)
+ $(PRINT_INSTALL) E-ACSL scripts
+ $(MKDIR) $(BINDIR)
+ $(CP) $(E_ACSL_DIR)/scripts/e-acsl-gcc.sh $(BINDIR)/
+ $(PRINT_INSTALL) E-ACSL man pages
+ $(MKDIR) $(MANDIR)/man1
+- $(CP) $(E_ACSL_DIR)/man/e-acsl-gcc.sh.1 $(MANDIR)/man1/
++ $(CPNX) $(E_ACSL_DIR)/man/e-acsl-gcc.sh.1 $(MANDIR)/man1/
+
+ uninstall::
+ $(PRINT_RM) E-ACSL share files
Index: pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure Tue Sep 5 07:30:00 2017
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_plugins_wp_configure,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+Recognize more recent coq.
+
+--- src/plugins/wp/configure~ 2017-06-01 08:02:09.000000000 +0000
++++ src/plugins/wp/configure
+@@ -2254,7 +2254,7 @@ fi
+ if test "$COQC" = "yes" ; then
+ COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([^ ]*\) .*$|\1|p' `
+ case $COQVERSION in
+- 8.4pl6|8.5*|trunk)
++ 8.4pl6|8.5*|8.6*|trunk)
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: coqc version $COQVERSION found" >&5
+ $as_echo "coqc version $COQVERSION found" >&6; }
+ ;;
Index: pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure.ac
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure.ac:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_configure.ac Tue Sep 5 07:30:00 2017
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_plugins_wp_configure.ac,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+Recognize more recent coq.
+
+--- src/plugins/wp/configure.ac~ 2017-06-01 08:02:17.000000000 +0000
++++ src/plugins/wp/configure.ac
+@@ -63,7 +63,7 @@ if test "$ENABLE_WP" != "no"; then
+ if test "$COQC" = "yes" ; then
+ COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
+ case $COQVERSION in
+- 8.4pl6|8.5*|trunk)
++ 8.4pl6|8.5*|8.6*|trunk)
+ AC_MSG_RESULT(coqc version $COQVERSION found)
+ ;;
+ *)
Index: pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v
diff -u /dev/null pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v:1.1
--- /dev/null Tue Sep 5 07:30:00 2017
+++ pkgsrc/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v Tue Sep 5 07:30:00 2017
@@ -0,0 +1,24 @@
+$NetBSD: patch-src_plugins_wp_share_coqwp_Zbits.v,v 1.1 2017/09/05 07:30:00 dholland Exp $
+
+Make this work with coq-8.6.
+
+--- src/plugins/wp/share/coqwp/Zbits.v~ 2017-06-01 08:02:13.000000000 +0000
++++ src/plugins/wp/share/coqwp/Zbits.v
+@@ -1868,7 +1868,7 @@ Local Ltac f_equal_hyp h f k :=
+ end.
+
+ Local Ltac linear2 :=
+- intros x y; (try split); intro H; (try split);
++ intros x y; (try split); intros H; (try split);
+ let k := fresh "k" in
+ Zbit_ext k;
+ try (destruct H as [H H0] ; f_equal_hyp H0 Zbit k; generalize H0; clear H0);
+@@ -1948,7 +1948,7 @@ Proof.
+ Qed.
+
+ Local Ltac linear3 :=
+- intros x y z; (try split); intro H; (try split);
++ intros x y z; (try split); intros H; (try split);
+ let k := fresh "k" in
+ Zbit_ext k;
+ try (destruct H as [H H0] ; f_equal_hyp H0 Zbit k; generalize H0; clear H0);
Home |
Main Index |
Thread Index |
Old Index