[why] New upstream release. Drop upstreamed -warning, -coq84, and -ocaml4 patches. Add -hashtbl patch. Ena
Jerry James
jjames at fedoraproject.org
Tue May 14 22:15:22 UTC 2013
commit 0769332a3245daaa3fc37f6763cbcd6b1ab62f12
Author: Jerry James <jamesjer at betterlinux.com>
Date: Tue May 14 16:14:50 2013 -0600
New upstream release.
Drop upstreamed -warning, -coq84, and -ocaml4 patches.
Add -hashtbl patch.
Enable Jessie plugin again.
.gitignore | 2 +-
gwhy-2.31.patch => gwhy-2.33.patch | 20 ++---
sources | 4 +-
why-2.31-coq84.patch | 27 ------
why-2.31-ocaml4.patch | 26 ------
why-2.31-warning.patch | 88 --------------------
...Makefile.in.patch => why-2.33-Makefile.in.patch | 9 ++-
why-2.33-hashtbl.patch | 51 +++++++++++
why.spec | 57 ++++++-------
9 files changed, 95 insertions(+), 189 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 719a194..5ad01f7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,2 @@
/krakatoa.pdf
-/why-2.31.tar.gz
+/why-2.33.tar.gz
diff --git a/gwhy-2.31.patch b/gwhy-2.33.patch
similarity index 68%
rename from gwhy-2.31.patch
rename to gwhy-2.33.patch
index c131f48..d106a7e 100644
--- a/gwhy-2.31.patch
+++ b/gwhy-2.33.patch
@@ -1,13 +1,13 @@
---- bin/gwhy.sh.orig 2012-07-19 12:33:10.000000000 -0600
-+++ bin/gwhy.sh 2012-07-30 20:23:41.708914796 -0600
+--- bin/gwhy.sh.orig 2013-04-20 00:34:04.000000000 -0600
++++ bin/gwhy.sh 2013-05-10 09:12:22.968553542 -0600
@@ -1,11 +1,17 @@
#!/bin/sh
-case $1 in
+if ! test $1; then
-+file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
++ file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
+else
-+file=$1
++ file=$1
+fi
+
+case $file in
@@ -22,15 +22,12 @@
echo "cd $d"
cd $d
jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
-@@ -13,20 +19,23 @@
+@@ -13,18 +19,20 @@
make -f $b.makefile gui
;;
*.c)
-- b=`basename $1 .c`
-- caduceus -why-opt -split-user-conj $1 || exit 1
-+ b=`basename $file .c`
-+ caduceus -why-opt -split-user-conj $file || exit 1
- make -f $b.makefile gui
+- frama-c -jessie -jessie-atp=gui -jessie-why-opt="-split-user-conj" $1 || exit 1
++ frama-c -jessie -jessie-atp=gui -jessie-why-opt="-split-user-conj" $file || exit 1
;;
*.jc)
- b=`basename $1 .jc`
@@ -41,10 +38,9 @@
*.mlw|*.why)
- gwhy-bin -split-user-conj $1
+ gwhy-bin -split-user-conj $file
-+ ;;
+ ;;
+ ?*)
+ echo "$file does not have file type extension recognized by gwhy"
- ;;
*)
- echo "don't know what to do with $1"
+ echo "gwhy needs the name of a file to inspect in order to run"
diff --git a/sources b/sources
index c472a51..17fa550 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
-08f92283da47fdb190f516339472e575 krakatoa.pdf
-d647f64049345be5654f8f3fdb077aa4 why-2.31.tar.gz
+c32c15249cc4d4f8b41638f551d9cc3f krakatoa.pdf
+25ad0493e0cd112f3fe5858aa605344a why-2.33.tar.gz
diff --git a/why-2.31-Makefile.in.patch b/why-2.33-Makefile.in.patch
similarity index 62%
rename from why-2.31-Makefile.in.patch
rename to why-2.33-Makefile.in.patch
index 9546b4b..2ea8cdb 100644
--- a/why-2.31-Makefile.in.patch
+++ b/why-2.33-Makefile.in.patch
@@ -1,10 +1,13 @@
---- Makefile.in.orig 2012-07-19 12:33:10.000000000 -0600
-+++ Makefile.in 2012-07-30 20:28:33.062463838 -0600
-@@ -812,14 +812,9 @@
+--- Makefile.in.orig 2013-04-20 00:34:04.000000000 -0600
++++ Makefile.in 2013-05-10 09:16:51.336053499 -0600
+@@ -804,17 +804,9 @@
mkdir -p $(LIBDIR)/why/coq7
cp -f $(VO7) $(LIBDIR)/why/coq7
install-coq-v8 install-coq-v8.1:
- if test -w $(COQLIB) ; then \
+- rm -f $(COQLIB)/user-contrib/Why*.v* ; \
+- rm -f $(COQLIB)/user-contrib/caduceus*.v* $(COQLIB)/user-contrib/Caduceus*.v* ; \
+- rm -f $(COQLIB)/user-contrib/jessie*.v* $(COQLIB)/user-contrib/Jessie*.v* ; \
- mkdir -p $(COQLIB)/user-contrib/Why ; \
- cp -f $(VO8) $(COQLIB)/user-contrib/Why ; \
- else \
diff --git a/why-2.33-hashtbl.patch b/why-2.33-hashtbl.patch
new file mode 100644
index 0000000..274c512
--- /dev/null
+++ b/why-2.33-hashtbl.patch
@@ -0,0 +1,51 @@
+--- ./jc/jc_annot_inference.ml.orig 2013-04-20 00:34:04.000000000 -0600
++++ ./jc/jc_annot_inference.ml 2013-05-14 12:29:30.199407024 -0600
+@@ -84,7 +84,7 @@ let forget_var_in_assertion v a =
+ let unfolding_of_app app =
+ let f = app.jc_app_fun in
+ let _, term_or_assertion =
+- try Hashtbl.find Jc_typing.logic_functions_table f.jc_logic_info_tag
++ try IntHashtblIter.find Jc_typing.logic_functions_table f.jc_logic_info_tag
+ with Not_found -> assert false
+ in
+ match term_or_assertion with
+@@ -2528,7 +2528,7 @@ let collect_expr_targets e =
+ in
+ let els = call.jc_call_args in
+ let _,_,fs,_ =
+- Hashtbl.find Jc_typing.functions_table fi.jc_fun_info_tag
++ IntHashtblIter.find Jc_typing.functions_table fi.jc_fun_info_tag
+ in
+ (* Collect preconditions of functions called. *)
+ let reqa = fs.jc_fun_requires in
+@@ -3543,7 +3543,7 @@ and ai_call iaio abs curinvs vio e =
+ (* Compute abstract value at function call *)
+ let curinvs = List.fold_left (ai_expr iaio abs) curinvs args in
+ let _f, _pos, spec, _body =
+- Hashtbl.find Jc_typing.functions_table f.jc_fun_info_tag
++ IntHashtblIter.find Jc_typing.functions_table f.jc_fun_info_tag
+ in
+ (* begin match body with None -> () | Some body -> *)
+ (* if Jc_options.interprocedural then *)
+@@ -3732,9 +3732,9 @@ and ai_function mgr iaio targets funpre
+
+ (* Add global variables as abstract variables in [env]. *)
+ let globvars =
+- Hashtbl.fold (fun _tag (vi,_e) acc ->
+- Vai.all_variables (new term_var vi) @ acc
+- ) Jc_typing.variables_table []
++ IntHashtblIter.fold (fun _tag (vi,_e) acc ->
++ Vai.all_variables (new term_var vi) @ acc
++ ) Jc_typing.variables_table []
+ in
+ let env = Environment.add env (Array.of_list globvars) [||] in
+
+@@ -4164,7 +4164,7 @@ let rec record_ai_inter_annotations mgr
+ (fun fi ->
+ let fi, _, fs, slo =
+ try
+- Hashtbl.find Jc_typing.functions_table fi.jc_fun_info_tag
++ IntHashtblIter.find Jc_typing.functions_table fi.jc_fun_info_tag
+ with Not_found -> assert false (* should never happen *)
+ in
+ match slo with
diff --git a/why.spec b/why.spec
index bea6607..8a5794c 100644
--- a/why.spec
+++ b/why.spec
@@ -19,14 +19,14 @@
%global debug_package %{nil}
Name: why
-Version: 2.31
-Release: 7%{?dist}
+Version: 2.33
+Release: 1%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
License: LPGLv2 with exceptions
URL: http://why.lri.fr/
-Source0: http://why.lri.fr/download/why-%{version}.tar.gz
+Source0: http://why.lri.fr/download/%{name}-%{version}.tar.gz
Source1: README.why-gwhy.Fedora
Source2: README.why-coq.Fedora
Source3: README.why
@@ -44,7 +44,7 @@ Source12: patch_jessie_pvs
# about when bad parameters are passed to it - this patch fixes that.
# Upstream has been informed about this issue and a better fix is on
# their todo list
-Patch0: gwhy-2.31.patch
+Patch0: gwhy-2.33.patch
# This patch makes a Fedora-specific fix to eliminate checking for the
# location of Coq - since we're using the coq package, we know where
@@ -52,16 +52,11 @@ Patch0: gwhy-2.31.patch
# It also makes a fix necessary to correctly build the bytecode only
# version of why by building the make_float_model tool correctly in
# this case.
-Patch1: %{name}-2.31-Makefile.in.patch
+Patch1: %{name}-2.33-Makefile.in.patch
-# The build system uses -warn-error, so we are forced to clean up warnings.
-Patch2: %{name}-2.31-warning.patch
-
-# Adapt to changes in OCaml 4.00.0.
-Patch3: %{name}-2.31-ocaml4.patch
-
-# Adapt to changes in coq 8.4.
-Patch4: %{name}-2.31-coq84.patch
+# Fix an incompletely converted hash table interface.
+# Sent upstream 14 May 2013.
+Patch2: %{name}-2.33-hashtbl.patch
BuildRequires: auto-destdir
BuildRequires: cvc3
@@ -89,8 +84,8 @@ BuildRequires: pvs
ExclusiveArch: %{ocaml_arches}
# Filter out names that should not be exposed externally
-%global __requires_exclude ocaml\\\(((Ast)|(Cc)|(Env)|(Error)|(Loc)|(Logic)|(Logic_decl)|(Misc)|(Parser)|(Project)|(Ptree)|(Types))\\\)
-%global __provides_exclude ocaml\\\(((Lexer)|(Lib)|(Loc)|(Output)|(Parser)|(Project)|(Report)|(Xml))\\\)
+%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Logic|Logic_decl|Misc|Ptree|Types)\\\)
+%global __provides_exclude ocaml\\\((Lexer|Lib|Output|Report|Xml)\\\)
%description
Why is a software verification platform that applies formal proving
@@ -223,14 +218,14 @@ based on Why, including various automated and interactive provers.
%patch0
%patch1
%patch2
-%patch3
-%patch4
cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
-# Fix missing DESTDIRs in the makefile
+# Add missing DESTDIRs and harden the build for network-using binaries
sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \
-e 's|$(PVSLIB)/why|$(DESTDIR)$(PVSLIB)/why|' \
+ -e '\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s/-o/-ccopt -Wl,-z,relro,-z,now &/' \
+ -e '/gtkThread\.cmx/s/-o/-ccopt -Wl,-z,relro,-z,now &/' \
-i Makefile.in
%define fix_encoding() \
@@ -251,9 +246,6 @@ for f in CHANGES COPYING examples/bresenham/bresenham.mlw \
%fix_encoding $f ISO-8859-1 UTF-8
done
-# Fix a doubly utf8-encoded file
-%fix_encoding examples/sqrt/sqrt_why.v UTF-8 ISO-8859-1
-
# Fix line endings
for f in examples-c/tutorial/average.c examples-c/tutorial/purse.c \
examples-c/ukkonen/main.c examples-c/ukkonen/ukkonen.c; do
@@ -274,14 +266,13 @@ sed -e "s|-I +apron|-I +apron -I +gmp|" \
%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif
-# Update the version numbers of external programs
+# Update acceptable version numbers of external programs
# Also, command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
-sed -e 's/\(versions_ok = \["0\.13\.0";"0\.14\.0";"0\.15\.1"\)\];/\1;"0.16.0";"0.16.1"];/' \
- -e 's/versions_ok = \["0\.93"\]/versions_ok = ["0.93";"0.95"]/' \
- -e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.36"]/' \
- -e 's/versions_ok = \["2.2"\]/versions_ok = ["2.4.1"]/' \
- -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.4pl1"]/' \
- -e 's/versions_ok = \["4\.1"\]/versions_ok = ["5.0"]/' \
+sed -e 's/"0\.16\.0"/&; "0.17.1"/' \
+ -e 's/"0\.94"/&; "0.95.1"/' \
+ -e 's/"1\.0\.24"/&; "1.0.38"/' \
+ -e 's/"8\.4"/&; "8.4pl2"/' \
+ -e 's/"4\.1"/&; "6.0"/' \
-e 's/command = "pvs"/command = "pvs-sbcl"/' \
-e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
-i tools/dpConfig.ml
@@ -296,7 +287,7 @@ make %{opt_option}
# Strip binaries (the Makefile misses some of them)
strip bin/why-cpulimit
-#strip frama-c-plugin/Jessie.cmxs
+strip frama-c-plugin/Jessie.cmxs
%if %opt
strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \
bin/why2html.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt
@@ -411,7 +402,7 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%files jessie
%{_bindir}/jessie
%{_libdir}/jessie/
-#%%{_libdir}/frama-c/plugins/Jessie.*
+%{_libdir}/frama-c/plugins/Jessie.*
%{_datadir}/applications/jessie.desktop
%if %{has_coq}
@@ -444,6 +435,12 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%changelog
+* Tue May 14 2013 Jerry James <loganjerry at gmail.com> - 2.33-1
+- New upstream release
+- Drop upstreamed -warning, -coq84, and -ocaml4 patches
+- Add -hashtbl patch
+- Enable Jessie plugin again
+
* Sat Feb 09 2013 Parag Nemade <paragn AT fedoraproject DOT org> - 2.31-7
- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077
More information about the scm-commits
mailing list