This is an automated email from the git hooks/post-receive script. mehdi pushed a commit to branch master in repository frama-c.
commit a7f89e5dc295621603d03eba6f3f9591b08a4b40 Author: Mehdi Dogguy <me...@debian.org> Date: Wed Dec 21 14:17:22 2016 +0100 Fix build on bytecode architectures - add patch debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch to make sure that LoopAnalysis appears before Value plugin during the linking phase. - add patch debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch to make sure that only bytecode files are used during a byte build. --- debian/changelog | 3 ++ .../0001-Fix-spelling-error-in-binary.patch | 1 - ...002-Use-bin-cp-instead-of-usr-bin-install.patch | 1 - .../0003-Disable-CHMOD_RO-invocations.patch | 1 - ...mlfind-package-lablgtk2-gnome.gnomecanvas.patch | 1 - ...005-Add-a-section-for-LoopAnalysis-plugin.patch | 36 ++++++++++++++++++++++ ...0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch | 35 +++++++++++++++++++++ debian/patches/series | 2 ++ 8 files changed, 76 insertions(+), 4 deletions(-) diff --git a/debian/changelog b/debian/changelog index 75c7805..c7f9337 100644 --- a/debian/changelog +++ b/debian/changelog @@ -2,6 +2,9 @@ frama-c (20161101+silicon+dfsg-2) UNRELEASED; urgency=medium * Disable apron * Add ocaml-findlib as a dependency for frama-c-base + * Fix build on bytecode architectures + - add patch debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch + - add patch debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch -- Mehdi Dogguy <me...@debian.org> Wed, 21 Dec 2016 13:08:38 +0100 diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch b/debian/patches/0001-Fix-spelling-error-in-binary.patch index bb43169..8177c60 100644 --- a/debian/patches/0001-Fix-spelling-error-in-binary.patch +++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch @@ -404,4 +404,3 @@ index 9ad708a..861dbda 100644 let arg_name="n" let default = 1000 end) --- diff --git a/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch b/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch index a18fd5a..0f57547 100644 --- a/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch +++ b/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch @@ -19,4 +19,3 @@ index 4c88e5c..0d9c74a 100644 CP_IF_DIFF = sh -c \ 'if cmp -s $$1 $$2; \ then touch -r $$2 $$1; \ --- diff --git a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch index 6b339f0..b5086f4 100644 --- a/debian/patches/0003-Disable-CHMOD_RO-invocations.patch +++ b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch @@ -19,4 +19,3 @@ index 0d9c74a..7d36c93 100644 CHMOD_RW= sh -c \ 'for f in "$$@"; do \ if test -e $$f; then chmod u+w $$f; fi \ --- diff --git a/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch b/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch index 2971b24..988c934 100644 --- a/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch +++ b/debian/patches/0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch @@ -19,4 +19,3 @@ index e254ddc..8068024 100644 else LIBRARY_NAMES_GUI = endif --- diff --git a/debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch b/debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch new file mode 100644 index 0000000..bccd556 --- /dev/null +++ b/debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch @@ -0,0 +1,36 @@ +From: Mehdi Dogguy <me...@debian.org> +Date: Wed, 21 Dec 2016 14:11:25 +0100 +Subject: Add a section for LoopAnalysis plugin + +Value plugin needs LoopAnalysis, but appears first during the linking +phase. In order to workaround that, we add a section for LoopAnalysis +just before the one for Value. +--- + Makefile | 14 ++++++++++++++ + 1 file changed, 14 insertions(+) + +diff --git a/Makefile b/Makefile +index abbc893..f6c8a2f 100644 +--- a/Makefile ++++ b/Makefile +@@ -745,6 +745,20 @@ PLUGIN_TESTS_DIRS:=callgraph + $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) + + ++################# ++# Loop Analysis # ++################# ++ ++PLUGIN_ENABLE:=$(ENABLE_CALLGRAPH) ++PLUGIN_DYNAMIC:=$(DYNAMIC_CALLGRAPH) ++PLUGIN_NAME:=Loop_Analysis ++PLUGIN_DISTRIBUTED:=yes ++PLUGIN_DIR:=src/plugins/loop_analysis ++PLUGIN_CMO:= options region_analysis_sig region_analysis region_analysis_stmt loop_analysis slevel_analysis register ++PLUGIN_INTERNAL_TEST:=yes ++$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) ++ ++ + ################## + # Value analysis # + ################## diff --git a/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch b/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch new file mode 100644 index 0000000..c8b5a85 --- /dev/null +++ b/debian/patches/0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch @@ -0,0 +1,35 @@ +From: Mehdi Dogguy <me...@debian.org> +Date: Wed, 21 Dec 2016 14:14:24 +0100 +Subject: gui.byte needs TARGETS_GUI_BYTE only + +--- + share/Makefile.dynamic | 8 ++++++-- + 1 file changed, 6 insertions(+), 2 deletions(-) + +diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic +index 9655220..0b60162 100644 +--- a/share/Makefile.dynamic ++++ b/share/Makefile.dynamic +@@ -197,8 +197,8 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) + TARGETS := $(TARGET_META) $(TARGET_CMI) + TARGETS_TOP := $(TARGET_TOP_CMO) $(TARGET_TOP_CMX) \ + $(TARGET_TOP_CMA) $(TARGET_TOP_CMXS) +-TARGETS_GUI := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO) \ +- $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS) ++TARGETS_GUI_BYTE := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO) ++TARGET_GUI := $(TARGETS_GUI_BYTE) $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS) + TARGETS_BYTE:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMO) $(TARGET_TOP_CMA) + TARGETS_OPT:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX) $(TARGET_TOP_CMXS) + +@@ -206,7 +206,11 @@ include $(MAKECONFIG_DIR)/Makefile.kernel + + byte:: $(TARGETS_BYTE) + opt:: $(TARGETS_OPT) ++ifeq ($(OCAMLBEST),byte) ++gui:: $(TARGETS_GUI_BYTE) ++else + gui:: $(TARGETS_GUI) ++endif + + # do not define additional targets if you come from the Frama-C Makefile + ifneq ($(FRAMAC_INTERNAL),yes) diff --git a/debian/patches/series b/debian/patches/series index 2d4205f..35d4b87 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -2,3 +2,5 @@ 0002-Use-bin-cp-instead-of-usr-bin-install.patch 0003-Disable-CHMOD_RO-invocations.patch 0004-Use-ocamlfind-package-lablgtk2-gnome.gnomecanvas.patch +0005-Add-a-section-for-LoopAnalysis-plugin.patch +0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch -- Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/frama-c.git _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits