diff options
author | dholland <dholland@pkgsrc.org> | 2017-09-05 07:30:00 +0000 |
---|---|---|
committer | dholland <dholland@pkgsrc.org> | 2017-09-05 07:30:00 +0000 |
commit | febd87649dab5d840890dfa649b74152cc4eb935 (patch) | |
tree | 813d2293c82fc47df97ac92b267cbb844aab9b39 | |
parent | 46f8bcf407ce7b6d53702f9707b26575bf252b37 (diff) | |
download | pkgsrc-febd87649dab5d840890dfa649b74152cc4eb935.tar.gz |
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".
-rw-r--r-- | devel/frama-c/Makefile | 24 | ||||
-rw-r--r-- | devel/frama-c/PLIST | 897 | ||||
-rw-r--r-- | devel/frama-c/distinfo | 19 | ||||
-rw-r--r-- | devel/frama-c/options.mk | 18 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-Makefile | 85 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-configure | 24 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-share_Makefile.common | 14 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c | 24 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile | 64 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-src_plugins_wp_configure | 15 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-src_plugins_wp_configure.ac | 15 | ||||
-rw-r--r-- | devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v | 24 |
12 files changed, 852 insertions, 371 deletions
diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile index a579eba6978..4d222cc34bf 100644 --- a/devel/frama-c/Makefile +++ b/devel/frama-c/Makefile @@ -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 -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" diff --git a/devel/frama-c/PLIST b/devel/frama-c/PLIST index d1ffd7a9b44..d1b72d0ec21 100644 --- a/devel/frama-c/PLIST +++ b/devel/frama-c/PLIST @@ -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.cmi ${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 diff --git a/devel/frama-c/distinfo b/devel/frama-c/distinfo index 341e2c90d28..95565ecec5f 100644 --- a/devel/frama-c/distinfo +++ b/devel/frama-c/distinfo @@ -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 diff --git a/devel/frama-c/options.mk b/devel/frama-c/options.mk index e9ee4ac2f6e..085baedc9fc 100644 --- a/devel/frama-c/options.mk +++ b/devel/frama-c/options.mk @@ -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 diff --git a/devel/frama-c/patches/patch-Makefile b/devel/frama-c/patches/patch-Makefile new file mode 100644 index 00000000000..9b6b5069427 --- /dev/null +++ b/devel/frama-c/patches/patch-Makefile @@ -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:: diff --git a/devel/frama-c/patches/patch-configure b/devel/frama-c/patches/patch-configure index 9e69dd25e61..6b6d3e1cf00 100644 --- a/devel/frama-c/patches/patch-configure +++ b/devel/frama-c/patches/patch-configure @@ -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; } + ;; diff --git a/devel/frama-c/patches/patch-share_Makefile.common b/devel/frama-c/patches/patch-share_Makefile.common new file mode 100644 index 00000000000..a83d010d107 --- /dev/null +++ b/devel/frama-c/patches/patch-share_Makefile.common @@ -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; \ diff --git a/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c b/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c new file mode 100644 index 00000000000..bc524f4212c --- /dev/null +++ b/devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c @@ -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 diff --git a/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile b/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile new file mode 100644 index 00000000000..1870ce52648 --- /dev/null +++ b/devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile @@ -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 diff --git a/devel/frama-c/patches/patch-src_plugins_wp_configure b/devel/frama-c/patches/patch-src_plugins_wp_configure new file mode 100644 index 00000000000..509324e8656 --- /dev/null +++ b/devel/frama-c/patches/patch-src_plugins_wp_configure @@ -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; } + ;; diff --git a/devel/frama-c/patches/patch-src_plugins_wp_configure.ac b/devel/frama-c/patches/patch-src_plugins_wp_configure.ac new file mode 100644 index 00000000000..cbf9ad00a06 --- /dev/null +++ b/devel/frama-c/patches/patch-src_plugins_wp_configure.ac @@ -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) + ;; + *) diff --git a/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v b/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v new file mode 100644 index 00000000000..01095802ec3 --- /dev/null +++ b/devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v @@ -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); |