.gitignore

@@ -0,0 +1,3 @@
+/why-2.29.tar.gz
+/krakatoa.pdf
+/caduceus.ps

README.why

@@ -0,0 +1,8 @@
+Fedora why package:
+
+Contains the main why executable and supporting tools.
+
+Consider visiting the main Why site - http://why.lri.fr - for more
+documentation. Also, there is more information about the tools
+Caduceus and Krakatoa at http://caduceus.lri.fr and
+http://krakatoa.lri.fr respectively.

README.why-coq.Fedora

@@ -0,0 +1,6 @@
+Fedora why-coq package:
+
+Contains libraries for interfacing why with Coq.
+
+You shouldn't have to do anything extra - you should now just be able
+to use the Coq-related capabilities of Why.

README.why-gwhy.Fedora

@@ -0,0 +1,6 @@
+Fedora why-gwhy package:
+
+Contains the gwhy GUI for Why.
+
+Run gwhy with "gwhy <filename>". (If you forget and run without a
+filename you'll be prompted for it.)

dead.package

@@ -1 +0,0 @@
-Abandoned by upstream and fails to build from source

div.pvs

@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+% 
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+% 
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+% 
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+div: THEORY
+BEGIN
+
+  x   : VAR int
+  nzy : VAR nzint
+
+  div(x, nzy): int =
+  IF (x >= 0 AND nzy > 0) THEN ndiv(x, nzy)
+  ELSIF (x >= 0 AND nzy < 0) THEN -ndiv(x, -nzy)
+  ELSIF (x < 0 AND nzy > 0) THEN -ndiv(-x, nzy)
+  ELSE ndiv(-x, -nzy)
+  ENDIF
+
+END div
+

gwhy-2.26.patch

@@ -0,0 +1,53 @@
+--- bin/gwhy.sh.orig	2011-03-02 01:27:41.000000000 -0700
++++ bin/gwhy.sh	2011-07-07 15:41:07.232455718 -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"`;
++else
++file=$1
++fi
++
++case $file in
+   *.java)
+-	b=`basename $1 .java`
+-	krakatoa $1 || exit 1
++	b=`basename $file .java`
++	krakatoa $file || exit 1
+ 	echo "krakatoa on $b.java done"
+-        d=`dirname $1`
++        d=`dirname $file`
+         echo "cd $d"
+         cd $d
+ 	jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
+@@ -13,20 +19,23 @@
+ 	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 $b.c || exit 1
+ 	make -f $b.makefile gui
+ 	;;
+   *.jc)
+-	b=`basename $1 .jc`
++	b=`basename $file .jc`
+ 	jessie -why-opt -split-user-conj $b.jc || exit 1
+ 	make -f $b.makefile gui
+ 	;;
+   *.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"
+ esac
+ 
+ 

gwhy.desktop

@@ -0,0 +1,8 @@
+[Desktop Entry]
+Encoding=UTF-8
+Name=gwhy
+Comment=Examine and develop Why .why files
+Exec=gwhy
+Icon=ICON-LOCATION-BASE/gwhy-icon.png
+Type=Application
+Categories=Development;

jessie.desktop

@@ -0,0 +1,8 @@
+[Desktop Entry]
+Encoding=UTF-8
+Name=jessie
+Comment=Verify C program using Jessie plug-in
+Exec=frama-c -jessie %f
+Icon=ICON-LOCATION-BASE/gwhy-icon.png
+Type=Application
+Categories=Development;

min.mlw

@@ -0,0 +1,4 @@
+logic min: int, int -> int
+axiom min_ax: forall x,y:int. min(x,y) <= x
+parameter r: int ref
+let f (n:int) = {} r := min !r n { r <= r@ }

min_why.why.result

@@ -0,0 +1,41 @@
+logic eq_unit : unit, unit -> prop
+
+logic neq_unit : unit, unit -> prop
+
+logic eq_bool : bool, bool -> prop
+
+logic neq_bool : bool, bool -> prop
+
+logic lt_int : int, int -> prop
+
+logic le_int : int, int -> prop
+
+logic gt_int : int, int -> prop
+
+logic ge_int : int, int -> prop
+
+logic eq_int : int, int -> prop
+
+logic neq_int : int, int -> prop
+
+logic add_int : int, int -> int
+
+logic sub_int : int, int -> int
+
+logic mul_int : int, int -> int
+
+logic neg_int : int -> int
+
+predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
+
+logic min : int, int -> int
+
+axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))
+
+goal f_po_1:
+  forall n:int.
+  forall r0:int.
+  forall r:int.
+  (r = min(r0, n)) ->
+  (r <= r0)
+

patch_jessie_pvs

@@ -0,0 +1,59 @@
+#!/bin/sh
+
+# To use PVS with frama-c without the NASA Langley PVS library:
+#   frama-c -jessie -jessie-atp pvs FILE.c  # Generates PVS files
+#   cd FILE.jessie/pvs
+#   patch_jessie_pvs # Patch jessie_why.pvs to not need NASA Langley library.
+# You can then run PVS to prove the generated theorems with:
+#   pvs-sbcl FILE_why.pvs
+#
+# Copyright (c) 2010 David A. Wheeler
+# 
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+# 
+# The above copyright notice and this permission notice shall be included in
+# all copies or substantial portions of the Software.
+# 
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+# THE SOFTWARE.
+
+
+if [ ! -f jessie_why.pvs ] ; then
+  echo "Did not find file jessie_why.pvs in current directory"
+  exit 1
+fi
+
+patch -p0 -N << END_OF_PATCH
+--- jessie_why.pvs.ORIGINAL	2010-10-05 14:41:58.965970651 -0400
++++ jessie_why.pvs	2010-10-06 14:28:39.250971269 -0400
+@@ -169,14 +169,14 @@
+     (FORALL (x: real): (FORALL (y: real): min(x, y) = x OR min(x, y) = y))
+ 
+   %% Why axiom sqrt_pos
+-  sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
++  % sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
+ 
+   %% Why axiom sqrt_sqr
+-  sqrt_sqr: AXIOM
+-    (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
++  % sqrt_sqr: AXIOM
++  %  (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
+ 
+   %% Why axiom sqr_sqrt
+-  sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
++  % sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
+ 
+   %% Why axiom abs_real_pos
+   abs_real_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES abs(x) = x))
+END_OF_PATCH
+

rem.pvs

@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+%
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+%
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+%
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+rem: THEORY
+BEGIN
+
+  x   : VAR int
+  nzy : VAR nzint
+
+  rem(x, nzy): int =
+  IF (x >= 0 AND nzy > 0) THEN rem(nzy)(x)
+  ELSIF (x >= 0 AND nzy < 0) THEN rem(-nzy)(x)
+  ELSIF (x < 0 AND nzy > 0) THEN -rem(nzy)(-x)
+  ELSE -rem(-nzy)(-x)
+  ENDIF
+
+END rem
+

sources

@@ -0,0 +1,3 @@
+34d8772de3d68c15a3a12935d90a0d60  krakatoa.pdf
+a7eb00d1f78e59221629604167eb3151  caduceus.ps
+cbb3b109a37f968bea9ffa6e43e3b822  why-2.29.tar.gz

why-2.28-Makefile.in.patch

@@ -0,0 +1,20 @@
+--- Makefile.in.orig	2011-03-02 01:27:41.000000000 -0700
++++ Makefile.in	2011-07-07 15:41:43.759455717 -0600
+@@ -844,14 +844,9 @@
+ 	cp -f $(V7FILES) $(LIBDIR)/why/coq7
+ 	cp -f $(VO7) $(LIBDIR)/why/coq7
+ install-coq-v8 install-coq-v8.1:
+-	if test -w $(COQLIB) ; then \
+-	  mkdir -p $(COQLIB)/user-contrib/Why ; \
+-	  cp -f $(VO8) $(COQLIB)/user-contrib/Why ; \
+-	else \
+-	  echo "Cannot copy to Coq standard library. Add \"-R $(LIBDIR)/why/coq Why\" to Coq options." ;\
+-	mkdir -p $(LIBDIR)/why/coq ;\
+-	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
+-	fi
++	mkdir -p $(COQLIB)/user-contrib/Why
++	cp -f $(V8FILES) $(COQLIB)/user-contrib/Why
++	cp -f $(VO8) $(COQLIB)/user-contrib/Why
+ 
+ install-pvs-no:
+ install-pvs-yes: $(PVSFILES)

why.spec

@@ -0,0 +1,536 @@
+# Whether coq is available
+%ifarch alpha %{arm} %{ix86} ia64 x86_64 ppc sparc sparcv9
+%global has_coq 1
+%else
+%global has_coq 0
+%endif
+
+# Whether PVS is available
+%ifarch %{ix86} x86_64 ppc sparcv9
+%global has_pvs 1
+%else
+%global has_pvs 0
+%endif
+
+# What kind of ocaml build to do
+%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
+
+# Don't create debuginfo; it's not particularly useful for OCaml programs.
+%global debug_package %{nil}
+
+Name:           why
+Version:        2.29
+Release:        2%{?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
+Source1:        README.why-gwhy.Fedora
+Source2:        README.why-coq.Fedora
+Source3:        README.why
+Source4:        gwhy.desktop
+Source5:        gwhy-icon.png
+Source6:        min.mlw
+Source7:        min_why.why.result
+Source8:        http://caduceus.lri.fr/manual/caduceus.ps
+Source9:        http://krakatoa.lri.fr/manual/krakatoa.pdf
+Source10:       jessie.desktop
+Source11:       div.pvs
+Source12:       rem.pvs
+Source13:       patch_jessie_pvs
+
+# The gwhy execution shell script is not particularly informative
+# 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.26.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
+# it is and their checking causes the rpm building to fail.
+# 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:         why-2.28-Makefile.in.patch
+
+BuildRequires:  auto-destdir
+BuildRequires:  cvc3
+BuildRequires:  desktop-file-utils
+BuildRequires:  emacs-nox xemacs-nox
+BuildRequires:  frama-c-devel
+BuildRequires:  gtk2-devel
+BuildRequires:  ocaml
+BuildRequires:  ocaml-camlp4-devel
+BuildRequires:  ocaml-lablgtk-devel
+BuildRequires:  ocaml-ocamldoc
+BuildRequires:  ocaml-ocamlgraph-devel
+%if %{has_coq}
+BuildRequires:  coq
+%endif
+%if %{has_pvs}
+BuildRequires:  pvs
+%endif
+
+# Only build on arches that support ocaml
+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))\\\)
+
+%description
+Why is a software verification platform that applies formal proving
+tools to annotated programs.  It is currently capable of analysis of C
+(through the included tool "Caduceus"), Java (through the included tool
+"Krakatoa"), and potentially ML programs with some modification into
+Why's own ML-like language.  Furthermore, Why is capable of analysis of
+any program that is mapped onto its own internal language.  It uses a
+weakest precondition involving calculus to generate potential theorems
+necessary for the proof of a program's correctness.  It translates these
+theorems into formats that can be used by external proof assistants
+(without any extra work Coq, PVS, HOL Light, and Mizar are supported -
+having one is recommended and both Coq and PVS are packaged for Fedora)
+and automated theorem provers (without any extra work Simplify,
+Alt-Ergo, Yices, Z3, CVC3, and Zenon are supported and Alt-Ergo, CVC3,
+and Zenon are packaged for Fedora) so that these results can be
+externally proven, resulting in a proof of program correctness.
+
+Note: Each user account must be set up by running "why-config" at the
+command line (to set up a configuration file).
+
+%package gwhy
+Group:          Applications/Engineering
+Summary:        IDE for Why software verification platform
+Requires:       %{name}%{?_isa} = %{version}-%{release}, zenity
+
+%description gwhy
+Gwhy is an optional graphical user interface for the Why software
+coordination platform.  It assists in the coordination of dispatching
+assertions that need to be proven to different theorem provers by
+providing an interface to do this and also supports inspection of why
+input files.
+
+%package jessie
+Group:          Applications/Engineering
+Summary:        Interface between why and frama-c
+Requires:       %{name}%{?_isa} = %{version}-%{release}
+Requires:       frama-c
+
+%description jessie
+The Jessie plugin, an interface between why and frama-c.  Invoke it with:
+  frama-c -jessie FILE.c
+
+%if %{has_coq}
+%package coq
+Group:          Applications/Engineering
+Summary:        Libraries for interfacing Coq with Why
+Requires:       %{name}%{?_isa} = %{version}-%{release}
+Requires:       coq
+
+%description coq
+This package contains a set of routines that assist in the manipulation
+of why Coq-formatted output within Coq.
+%endif
+
+%if %{has_pvs}
+# Why's integration with PVS depends on the NASA Langley PVS Libraries,
+# which have no license information.  This provides an alternative:
+%package pvs-support
+Group:          Applications/Engineering
+Summary:        Complete Why software verification platform suite
+Requires:       %{name}%{?_isa} = %{version}-%{release}
+Requires:       pvs
+
+%description pvs-support
+This package provides support definitions so that the Why software
+verification platform suite can invoke PVS without licensing issues.
+%endif
+
+%package emacs
+Summary:        Emacs support file for why files
+Group:          Development/Languages
+Requires:       %{name} = %{version}-%{release}
+Requires:       emacs(bin)
+BuildArch:      noarch
+
+%description emacs
+This package contains an Emacs support file for working with why files.
+
+%package emacs-el
+Summary:        Emacs source file for why support
+Group:          Development/Languages
+Requires:       %{name}-emacs = %{version}-%{release}
+BuildArch:      noarch
+
+%description emacs-el
+This package contains the Emacs source file for the Emacs why support.
+This package is not needed to use the Emacs support.
+
+%package xemacs
+Summary:        XEmacs support file for why files
+Group:          Development/Languages
+Requires:       %{name} = %{version}-%{release}
+Requires:       xemacs(bin)
+BuildArch:      noarch
+
+%description xemacs
+This package contains an XEmacs support file for working with why files.
+
+%package xemacs-el
+Summary:        XEmacs source file for why support
+Group:          Development/Languages
+Requires:       %{name}-xemacs = %{version}-%{release}
+BuildArch:      noarch
+
+%description xemacs-el
+This package contains the XEmacs source file for the XEmacs why support.
+This package is not needed to use the Emacs support.
+
+%package all
+Group:          Applications/Engineering
+Summary:        Complete Why software verification platform suite
+Requires:       why%{?_isa} = %{version}-%{release}
+Requires:       why-gwhy%{?_isa} = %{version}-%{release}
+Requires:       why-jessie%{?_isa} = %{version}-%{release}
+%if %{has_coq}
+Requires:       why-coq%{?_isa} = %{version}-%{release}
+%endif
+%if %{has_pvs}
+Requires:       why-pvs-support%{?_isa} = %{version}-%{release}
+%endif
+Requires:       alt-ergo cvc3 gappa zenon
+
+%description all
+This package provides a complete software verification platform suite
+based on Why, including various automated and interactive provers.
+
+%prep
+%setup -q
+%patch0
+%patch1
+
+cp -p %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 %SOURCE11 %SOURCE12 %SOURCE13 ./
+
+# Fix missing DESTDIRs in the makefile
+sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \
+    -e 's|$(PVSLIB)/why|$(DESTDIR)$(PVSLIB)/why|' \
+    -i Makefile.in
+
+%define fix_encoding() \
+  iconv -f %2 -t %3 %1 > %1.utf8; \
+  touch -r %1 %1.utf8; \
+  mv -f %1.utf8 %1;
+
+# Fix encodings
+for f in CHANGES COPYING examples/bresenham/bresenham.mlw \
+  examples/bresenham/bresenham_coq.mlw examples/bresenham/bresenham_inv.mlw \
+  examples/edit-distance/distance.mlw examples/heapsort/downheap.mlw \
+  examples/heapsort/heapsort.mlw examples/heapsort/Inftree.v \
+  examples/kmp/kmp.mlw examples/kmp/Lex.v examples/kmp/Match.v \
+  examples/kmp/Next.v examples/misc/matrix.why examples/misc/matrix_why.v \
+  examples/quicksort/partition.mlw examples/quicksort/Partition.v \
+  examples/quicksort/quicksort.mlw examples/quicksort/Quicksort.v \
+  examples/sqrt/sqrt.mlw examples/string-matching/Match.v; do
+  %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
+  sed "s/\r//" $f > $f.new
+  touch -r $f $f.new
+  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|" \
+    -i configure
+
+%build
+%if ! %{opt}
+%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
+%else
+%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
+%endif
+
+# Update the 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"\]/versions_ok = ["0.15.0"]/' \
+    -e 's/versions_ok = \["0\.91";.*\]/versions_ok = ["0.93"]/' \
+    -e 's/versions_ok = \["1\.0\.17";.*\]/versions_ok = ["1.0.29"]/' \
+    -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.3pl2"]/' \
+    -e 's/versions_ok = \["4\.1"\]/versions_ok = ["5.0"]/' \
+    -e 's/command = "pvs"/command = "pvs-sbcl"/' \
+    -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
+    -i tools/dpConfig.ml
+sed -e 's/pvs/pvs-sbcl/' -i configure
+
+%if %{has_coq}
+%configure --enable-verbosemake
+%else
+%configure --enable-verbosemake COQC=no
+%endif
+make %{opt_option}
+
+# Strip binaries (the Makefile misses some of them)
+strip bin/why-cpulimit
+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
+%endif
+
+%install
+make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib
+
+# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
+%if ! %{has_coq}
+rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
+%endif
+
+# If no PVS, no .pvs files should be installed
+%if ! %{has_pvs}
+rm -fr %{buildroot}%{_libdir}/pvs
+%endif
+
+# Install desktop icon and menu entry
+%global why_data_dir %{_datadir}/why
+mkdir -p %{buildroot}%{why_data_dir}
+cp -p gwhy-icon.png %{buildroot}%{why_data_dir}
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i gwhy.desktop
+desktop-file-install --vendor="fedora" \
+ --dir=%{buildroot}%{_datadir}/applications gwhy.desktop
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i jessie.desktop
+desktop-file-install --vendor="fedora" \
+ --dir=%{buildroot}%{_datadir}/applications jessie.desktop
+
+%if %{has_pvs}
+# Get rid of a BUILDROOT reference in a log file (fails QA_CHECK_RPATHS)
+sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out
+
+mkdir -p               %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p div.pvs rem.pvs  %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p patch_jessie_pvs %{buildroot}%{_bindir}/
+%endif
+
+%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}
+%global why_examples_dir %{why_doc_dir}/examples/
+
+# Fix up documentation and examples
+mkdir -p %{buildroot}%{why_examples_dir}mlw/
+mkdir -p %{buildroot}%{why_examples_dir}c/
+cp -p doc/manual.ps %{buildroot}%{why_doc_dir}/why-manual.ps
+cp -p caduceus.ps krakatoa.pdf README.why CHANGES COPYING LICENSE README Version %{buildroot}%{why_doc_dir}
+
+# Copy in the example files, leaving behind all generated files
+cd examples
+for d in `find -mindepth 1 -maxdepth 1 -type d`; do
+ mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
+done
+for f in `find -regex '.*\(\.mlw\|\.why\)' | grep -E -v '_inv|_coq|_why'`; do
+ cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
+done
+
+cd ../examples-c
+for d in `find -mindepth 1 -maxdepth 1 -type d`; do
+ mkdir -p %{buildroot}%{why_examples_dir}c/$d
+done
+for f in `find -regex '.*\.c'`; do
+ cp -p $f %{buildroot}%{why_examples_dir}c/$f
+done
+
+# Remove a stray coq file (already installed in the right place)
+rm -f %{buildroot}%{_libdir}/coq/jessie_why.v
+
+# Move the Emacs support file to the right places and byte compile it
+cd ..
+mkdir -p %{buildroot}%{_emacs_sitelispdir}
+cp -p lib/emacs/why.el %{buildroot}%{_emacs_sitelispdir}
+mkdir -p %{buildroot}%{_xemacs_sitelispdir}
+cp -p lib/emacs/why.el %{buildroot}%{_xemacs_sitelispdir}
+cd %{buildroot}%{_emacs_sitelispdir}
+%{_emacs_bytecompile} why.el
+cd %{buildroot}%{_xemacs_sitelispdir}
+%{_xemacs_bytecompile} why.el
+rm -fr %{buildroot}%{_libdir}/why/emacs
+
+%check
+%if %opt
+%global why bin/why.opt
+%else
+%global why bin/why.byte
+%endif
+WHYLIB=lib %why --why --output min.why min.mlw
+diff -u min.why min_why.why.result  # Show differences from correct result.
+
+%files
+%{_bindir}/*
+%{_libdir}/caduceus/
+%{_libdir}/why/
+%{_mandir}/man1/why.1*
+%{why_doc_dir}/
+# This last example is really an example only for Coq - only .v files
+%exclude %{why_examples_dir}mlw/string-matching/
+# why-gwhy:
+%exclude %{_bindir}/gwhy*
+# why-jessie
+%exclude %{_bindir}/jessie
+# why-pvs-support:
+%exclude %{_bindir}/patch_jessie_pvs
+# why-coq:
+%exclude %{_libdir}/caduceus/coq/
+
+%files gwhy
+%doc README.why-gwhy.Fedora
+%{_bindir}/gwhy
+%{_bindir}/gwhy-bin
+%{why_data_dir}/
+%{_datadir}/applications/fedora-gwhy.desktop
+
+%files jessie
+%{_bindir}/jessie
+%{_libdir}/jessie/
+%{_libdir}/frama-c/plugins/Jessie.*
+%{_datadir}/applications/fedora-jessie.desktop
+
+%if %{has_coq}
+%files coq
+%doc README.why-coq.Fedora
+%{_libdir}/coq/user-contrib/Why/
+%{_libdir}/caduceus/coq/
+%endif
+
+%if %{has_pvs}
+%files pvs-support
+%{_libdir}/pvs/lib/*
+%{_bindir}/patch_jessie_pvs
+%endif
+
+%files emacs
+%{_emacs_sitelispdir}/why.elc
+
+%files emacs-el
+%{_emacs_sitelispdir}/why.el
+
+%files xemacs
+%{_xemacs_sitelispdir}/why.elc
+
+%files xemacs-el
+%{_xemacs_sitelispdir}/why.el
+
+# "why-all" is a meta-package; it just depends on other packages, so that
+# it's easier to install a useful suite of tools.  Thus, it has no files:
+%files all
+
+
+%changelog
+* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 2.29-2
+- Fix broken conditionals
+
+* Mon Jul 11 2011 Jerry James <loganjerry@gmail.com> - 2.29-1
+- New upstream release (fixes FTBFS: bz 715902)
+- Remove unnecessary spec file elements (BuildRoot, etc.)
+- Update approach to filtering provides and requires
+- Add has_pvs analogously to has_coq, and simplify macro usage
+- Add (X)Emacs support packages
+- New subpackage for the jessie plugin to avoid unowned directories and
+  permit a direct dependency on frama-c
+- Prepare for the eventual availability of APRON
+
+* Thu Apr 14 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.2
+- add ppc to excludearch, too. No pvs-sbcl available there
+
+* Wed Apr 13 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.1
+- add ppc64 to excludearch, no sbcl available there
+
+* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.28-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
+
+* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.28-1
+- Since 2.26 FTBFS, try latest upstream (2.28).
+- Rebase Makefile.in patch.
+- Fix(?) test result.
+- No libdir/frama-c directory is created any more.
+
+* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.26-2
+- Bump and rebuild for OCaml 3.12.
+
+* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler@dwheeler.com> - 2.26-1
+- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf)
+- Integrated with Frama-C and PVS (as pvs-sbcl)
+
+* Mon Jan 11 2010 Richard W.M. Jones <rjones@gmail.com> - 2.23-2
+- Rebuild to fix dependencies.
+
+* Fri Jan 08 2010 Alan Dunn <amdunn@gmail.com> - 2.23-1
+- Upgrade to upstream version 2.23
+- Move execstack fixing to spec file from patch
+- Moved patch descriptions to initial patch declaration as in examples
+  in Fedora documentation
+- New Caduceus, Krakatoa documentation
+- Update test result from small test min.mlw
+- Added CVC3 interfacing capabilities
+- Removed patch for gwhy configuration, as there is a new mechanism for this
+
+* Tue Sep 22 2009 Dennis Gilmore <dennis@ausil.us> - 2.17-5
+- Exclude sparc64 s390 s390x  there is no ocaml there
+
+* Fri Aug 07 2009 Alan Dunn <amdunn@gmail.com> - 2.17-4
+- Removed now irrelevant check for no OCaml in Fedora < 9 (those
+  distributions are EOL)
+- Changed ExcludeArch to proper Fedora versions
+- Builds coq subpackage exactly when Coq can be built, thus making
+  build independent of whether Coq can be built
+- define -> global
+- Fixed accidental use of in tar ocamlgraph instead of one that is
+  separately packaged
+
+* Mon Jul 27 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
+
+* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
+
+* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 2.17-1
+- Upgrade to version 2.17 (bz: 477790)
+- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
+- Minor filename change in 2.17 (GPL -> LICENSE)
+- Added back Coq .v files to match policy for Coq
+- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
+- Minor changes to patches to ensure they still work in 2.17
+- Corrected package location gwhy-icon.png (should only be in gwhy)
+* Tue Aug 5 2008 Alan Dunn <amdunn@gmail.com> 2.14-2.1
+- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
+* Fri Aug 1 2008 Alan Dunn <amdunn@gmail.com> 2.14-2
+- Fixed minor issues in response to package review:
+- Inclusion of COPYING, GPL license-related files
+- Added config.mll patch to make default config file created nicer
+- Changes subpackage dependencies to be fully versioned.
+- Makes during build allowed to be noisy (allowed to print).
+* Wed Jul 30 2008 Alan Dunn <amdunn@gmail.com> 2.14-1
+- Changed to new version of why, removed previous why-cpulimit name
+  change, zenon output format patches as the issues were fixed in
+  why 2.14.
+- Moved doc subpackage back into main package.
+- Added example files to documentation subpackage.
+- Added check section with test on small why file.
+- Reformatted some macro names for greater readability.
+* Thu Jul 24 2008 Alan Dunn <amdunn@gmail.com> 2.13-2
+- Added several patches: fixed Zenon output, completed fix of rename
+  of cpulimit -> why-cpulimit.
+* Wed Jul 23 2008 Alan Dunn <amdunn@gmail.com> 2.13-1
+- Initial Fedora RPM version.
+
+# TODO:
+# If file $HOME/.gwhyrc does not exist, autorun "why-config".
+# Finish packaging/integrating "APRON" (for Inference of annotations)
+