[why] Rebuild with APRON and gappalib-coq support.

[Jerry James]

commit 7d0ca0e460f2fcc6bd30bef27f98af35b42defca
Author: Jerry James <loganjerry at gmail.com>
Date:   Wed Nov 23 13:56:43 2011 -0700

    Rebuild with APRON and gappalib-coq support.

 why-apron.patch |   40 ++++++++++++++++++++++++++++++++++++++++
 why.spec        |   22 ++++++++++++++--------
 2 files changed, 54 insertions(+), 8 deletions(-)
---
diff --git a/why-apron.patch b/why-apron.patch
new file mode 100644
index 0000000..4e23767
--- /dev/null
+++ b/why-apron.patch
@@ -0,0 +1,40 @@
+--- jc/jc_annot_inference.ml.orig	2011-10-24 09:21:06.000000000 -0600
++++ jc/jc_annot_inference.ml	2011-11-23 13:47:40.438177237 -0700
+@@ -148,7 +148,7 @@
+ 	      Some(tptr,offt)
+ 	end
+     | JCTvar _ | JCTderef _ | JCTapp _ | JCTold _ | JCTat _ | JCTif _ 
+-    | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
++    | JCTlet _ | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
+     | JCTconst _ | JCTbinary _ | JCTunary _ | JCToffset _ | JCTinstanceof _ 
+     | JCTreal_cast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTcast _ ->
+ 	None
+@@ -491,7 +491,7 @@
+   in
+   Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
+   let formula = Format.flush_str_formatter () in
+-  let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
++  let lab = Output.old_reg_pos "G" ?id ?kind ?name ~formula (Loc.extract loc) in
+   new assertion_with ~mark:lab a
+ 
+ 
+@@ -608,8 +608,8 @@
+ 	Atp.Fn(atp_of_unop uop, [atp_of_term t1])
+     | JCTvar _ | JCTderef _ | JCTapp _ | JCToffset _ ->
+ 	Atp.Var (Vwp.variable_for_term t)
+-    | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ 
+-    | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _ 
++    | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ | JCTlet _
++    | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _
+     | JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _ ->
+ 	err ()
+ 
+@@ -1198,7 +1198,7 @@
+       | JCTunary _ | JCTshift _ | JCTinstanceof _ | JCTmatch _ 
+       | JCTold _ | JCTat _ | JCTcast _ | JCTbitwise_cast _ 
+       | JCTrange_cast _ | JCTreal_cast _ | JCTaddress _ | JCTbase_block _
+-      | JCTrange _ | JCTif _ -> 
++      | JCTlet _ | JCTrange _ | JCTif _ -> 
+ 	  err ()
+     with Failure "linearize" -> 
+       (TermMap.add t (Int 1) TermMap.empty, Int 0)
diff --git a/why.spec b/why.spec
index d300b90..4f1ef57 100644
--- a/why.spec
+++ b/why.spec
@@ -54,14 +54,19 @@ Patch0:         gwhy-2.26.patch
 # this case.
 Patch1:         why-2.30-Makefile.in.patch
 
+# This patch fixes some mildly bitrotted APRON support code.
+# It will be sent upstream.
+Patch2:         why-apron.patch
+
 BuildRequires:  auto-destdir
 BuildRequires:  cvc3
 BuildRequires:  desktop-file-utils
 BuildRequires:  emacs-nox xemacs xemacs-packages-extra
-BuildRequires:  flocq
 BuildRequires:  frama-c-devel
+BuildRequires:  gappalib-coq
 BuildRequires:  gtk2-devel
 BuildRequires:  ocaml
+BuildRequires:  ocaml-apron-devel
 BuildRequires:  ocaml-camlp4-devel
 BuildRequires:  ocaml-lablgtk-devel
 BuildRequires:  ocaml-ocamldoc
@@ -127,7 +132,7 @@ The Jessie plugin, an interface between why and frama-c.  Invoke it with:
 Group:          Applications/Engineering
 Summary:        Libraries for interfacing Coq with Why
 Requires:       %{name}%{?_isa} = %{version}-%{release}
-Requires:       coq, flocq
+Requires:       gappalib-coq
 
 %description coq
 This package contains a set of routines that assist in the manipulation
@@ -200,7 +205,7 @@ Requires:       why-coq%{?_isa} = %{version}-%{release}
 %if %{has_pvs}
 Requires:       why-pvs-support%{?_isa} = %{version}-%{release}
 %endif
-Requires:       alt-ergo cvc3 gappa zenon
+Requires:       alt-ergo cvc3 gappalib-coq zenon
 
 %description all
 This package provides a complete software verification platform suite
@@ -210,6 +215,7 @@ based on Why, including various automated and interactive provers.
 %setup -q
 %patch0
 %patch1
+%patch2
 
 cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
 
@@ -247,9 +253,6 @@ for f in examples-c/tutorial/average.c examples-c/tutorial/purse.c \
   mv -f $f.new $f
 done
 
-# APRON support: fix some warnings that -warn-error turns into errors
-sed -i "s/| JCTrange _/| JCTlet _ | JCTrange _/" jc/jc_annot_inference.ml
-
 # APRON support: add a missing include and a missing rpath
 sed -e "s|-I +apron|-I +apron -I +mlgmpidl|" \
     -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
@@ -274,9 +277,9 @@ sed -e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.30"]/' \
 sed -e 's/pvs/pvs-sbcl/' -i configure
 
 %if %{has_coq}
-%configure --enable-verbosemake
+%configure --enable-apron --enable-verbosemake
 %else
-%configure --enable-verbosemake COQC=no
+%configure --enable-apron --enable-verbosemake COQC=no
 %endif
 make %{opt_option}
 
@@ -430,6 +433,9 @@ diff -u min.why min_why.why.result  # Show differences from correct result.
 
 
 %changelog
+* Wed Nov 23 2011 Jerry James <loganjerry at gmail.com> - 2.30-2
+- Rebuild with APRON and gappalib-coq support
+
 * Fri Oct 28 2011 Jerry James <loganjerry at gmail.com> - 2.30-1
 - New upstream release