[Pkg-ocaml-maint-commits] [frama-c] 03/08: Avoid double linking of LoopAnalysis.cmo

[Mehdi Dogguy]

This is an automated email from the git hooks/post-receive script.

mehdi pushed a commit to branch master
in repository frama-c.

commit d991c20b71db2d46a1fed561c8f78fa2eef20940
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Tue Dec 27 23:23:36 2016 +0100

    Avoid double linking of LoopAnalysis.cmo
---
 debian/changelog                                   |  1 +
 ...005-Add-a-section-for-LoopAnalysis-plugin.patch | 36 ----------------------
 .../0005-Value.cmo-needs-LoopAnalysis.cmo.patch    | 26 ++++++++++++++++
 debian/patches/series                              |  2 +-
 4 files changed, 28 insertions(+), 37 deletions(-)

diff --git a/debian/changelog b/debian/changelog
index 18b37c5..b8e82c2 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -3,6 +3,7 @@ frama-c (20161101+silicon+dfsg-3) UNRELEASED; urgency=medium
   * Fix typo in Vcs-Browser field
   * Install frama-c-config utility in frama-c-base
   * Clean up content of filtered files from debian/gbp.conf
+  * Avoid double linking of LoopAnalysis.cmo
 
  -- Mehdi Dogguy <mehdi at debian.org>  Thu, 22 Dec 2016 10:06:03 +0100
 
diff --git a/debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch b/debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch
deleted file mode 100644
index bccd556..0000000
--- a/debian/patches/0005-Add-a-section-for-LoopAnalysis-plugin.patch
+++ /dev/null
@@ -1,36 +0,0 @@
-From: Mehdi Dogguy <mehdi at 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/0005-Value.cmo-needs-LoopAnalysis.cmo.patch b/debian/patches/0005-Value.cmo-needs-LoopAnalysis.cmo.patch
new file mode 100644
index 0000000..879a1db
--- /dev/null
+++ b/debian/patches/0005-Value.cmo-needs-LoopAnalysis.cmo.patch
@@ -0,0 +1,26 @@
+From: Mehdi Dogguy <mehdi at debian.org>
+Date: Wed, 21 Dec 2016 14:11:25 +0100
+Subject: Value.cmo needs LoopAnalysis.cmo
+
+Value plugin needs LoopAnalysis, but appears first during the linking
+phase. In order to workaround that, we move it before Value.cmo in the
+PLUGIN_CMO_LIST variable.
+---
+ Makefile | 4 ++++
+ 1 file changed, 4 insertions(+)
+
+diff --git a/Makefile b/Makefile
+index abbc8935..6fdf3357 100644
+--- a/Makefile
++++ b/Makefile
+@@ -1095,6 +1095,10 @@ $(foreach p,$(EXTERNAL_PLUGINS),$(eval $(call INCLUDE_PLUGIN,$p)))
+ CMX	= $(CMO:.cmo=.cmx)
+ CMI	= $(CMO:.cmo=.cmi)
+ 
++PLUGIN_CMO_LIST:=$(subst $(PWD)/lib/plugins/top/Value.cmo,\
++	$(PWD)/lib/plugins/top/LoopAnalysis.cmo $(PWD)/lib/plugins/top/Value.cmo,\
++	$(filter-out $(PWD)/lib/plugins/top/LoopAnalysis.cmo, $(PLUGIN_CMO_LIST)))
++
+ ALL_CMO	= $(CMO) $(PLUGIN_CMO_LIST) $(STARTUP_CMO)
+ ALL_CMX	= $(CMX) $(PLUGIN_CMX_LIST) $(STARTUP_CMX)
+ 
diff --git a/debian/patches/series b/debian/patches/series
index 35d4b87..d83414e 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -2,5 +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
+0005-Value.cmo-needs-LoopAnalysis.cmo.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