[Pkg-ocaml-maint-commits] [SCM] why packaging branch, master, updated. debian/2.30+dfsg-2-3-g6c73a70

[Mehdi Dogguy]

The following commit has been merged in the master branch:
commit cf2cd8089369ad06ebb3ec672a7df15a00094e1b
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Mon Jan 16 18:25:11 2012 +0100

    Fix caduceus/frama-c issue

diff --git a/debian/changelog b/debian/changelog
index 8ff4ec6..37351e3 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -4,8 +4,11 @@ why (2.30+dfsg-3) unstable; urgency=low
     - Adapt version_regexp because "alt-ergo -version" changed.
   * Fix 0004-Default-to-why2-for-jessie-atp.patch
     - default to "gui" instead of "why2".
+  * Add 0007-Replace-caduceus-invocation-by-Frama-C.patch
+    - Caduceus is gone. We use Frama-C instead.
+    - Adding Frama-C to Why's dependencies.
 
- -- Mehdi Dogguy <mehdi at debian.org>  Mon, 16 Jan 2012 18:08:14 +0100
+ -- Mehdi Dogguy <mehdi at debian.org>  Mon, 16 Jan 2012 18:19:38 +0100
 
 why (2.30+dfsg-2) unstable; urgency=low
 
diff --git a/debian/control b/debian/control
index 6bdc5ed..7cc5077 100644
--- a/debian/control
+++ b/debian/control
@@ -30,6 +30,7 @@ Depends:
   ${shlibs:Depends},
   ${ocaml:Depends},
   ${misc:Depends},
+  frama-c-base (= ${F:FramaCVersion}),
   make
 Suggests: libwhy-coq (= ${binary:Version})
 Recommends: alt-ergo
diff --git a/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch b/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch
new file mode 100644
index 0000000..0e130b2
--- /dev/null
+++ b/debian/patches/0007-Replace-caduceus-invocation-by-Frama-C.patch
@@ -0,0 +1,24 @@
+From: Mehdi Dogguy <mehdi at debian.org>
+Date: Mon, 16 Jan 2012 18:19:16 +0100
+Subject: Replace caduceus invocation by Frama-C
+
+---
+ bin/gwhy.sh |    4 +---
+ 1 files changed, 1 insertions(+), 3 deletions(-)
+
+diff --git a/bin/gwhy.sh b/bin/gwhy.sh
+index 35c487e..f7d7a6b 100755
+--- a/bin/gwhy.sh
++++ b/bin/gwhy.sh
+@@ -13,9 +13,7 @@ case $1 in
+ 	make -f $b.makefile gui
+ 	;;
+   *.c)
+-	b=`basename $1 .c`
+-	caduceus -why-opt -split-user-conj $1 || exit 1
+-	make -f $b.makefile gui
++	frama-c -jessie -jessie-why-opt="-split-user-conj" $1 || exit 1
+ 	;;
+   *.jc)
+ 	b=`basename $1 .jc`
+-- 
diff --git a/debian/patches/series b/debian/patches/series
index 189bddd..3d379b7 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -4,3 +4,4 @@
 0004-Default-to-why2-for-jessie-atp.patch
 0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
 0006-Fix-spelling-error-in-binary.patch
+0007-Replace-caduceus-invocation-by-Frama-C.patch
diff --git a/debian/rules b/debian/rules
index 01a51d0..9cfe3a6 100755
--- a/debian/rules
+++ b/debian/rules
@@ -8,6 +8,7 @@ include /usr/share/coq/coqvars.mk
 
 WHYDIR    = $(CURDIR)/debian/why
 FRAMADIR  = $(WHYDIR)/$(shell frama-c -print-plugin-path)
+FRAMAVER  = $(shell dpkg-query -W -f='$${Version}' frama-c-base)
 VERSION   = $(shell cat Version | grep ^VERSION | cut -d= -f 2)
 export OCAMLINIT_SED += -e 's/@VERSION@/$(VERSION)/g'
 
@@ -41,6 +42,7 @@ override_dh_auto_install:
 	#Jessie.cma is installed, no need for this extra file
 	-$(RM) -f $(FRAMADIR)/Jessie.cmo
 	echo 'F:CoqABI=$(COQ_ABI)' >> debian/libwhy-coq.substvars
+	echo 'F:FramaCVersion=$(FRAMAVER)' >> debian/why.substvars
 
 override_dh_compress:
 	dh_compress -X.v -X.sx -X.why

-- 
why packaging