[Pkg-ocaml-maint-commits] [frama-c] 03/04: Fix build on bytecode architectures

Mehdi Dogguy mehdi at moszumanska.debian.org
Wed Dec 21 13:25:32 UTC 2016


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 <mehdi at 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 <mehdi at 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 <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/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 <mehdi at 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



More information about the Pkg-ocaml-maint-commits mailing list