The following commit has been merged in the master branch:
commit cf2cd8089369ad06ebb3ec672a7df15a00094e1b
Author: Mehdi Dogguy <me...@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 <me...@debian.org>  Mon, 16 Jan 2012 18:08:14 +0100
+ -- Mehdi Dogguy <me...@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 <me...@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

_______________________________________________
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

Reply via email to