diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..02ffd25 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +/why-2.29.tar.gz +/krakatoa.pdf +/caduceus.ps diff --git a/README.why b/README.why new file mode 100644 index 0000000..ba95dfa --- /dev/null +++ b/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. \ No newline at end of file diff --git a/README.why-coq.Fedora b/README.why-coq.Fedora new file mode 100644 index 0000000..406a7a9 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/README.why-gwhy.Fedora b/README.why-gwhy.Fedora new file mode 100644 index 0000000..3cc41b4 --- /dev/null +++ b/README.why-gwhy.Fedora @@ -0,0 +1,6 @@ +Fedora why-gwhy package: + +Contains the gwhy GUI for Why. + +Run gwhy with "gwhy ". (If you forget and run without a +filename you'll be prompted for it.) \ No newline at end of file diff --git a/dead.package b/dead.package deleted file mode 100644 index 497866a..0000000 --- a/dead.package +++ /dev/null @@ -1 +0,0 @@ -Abandoned by upstream and fails to build from source diff --git a/div.pvs b/div.pvs new file mode 100644 index 0000000..4005fe3 --- /dev/null +++ b/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 + diff --git a/gwhy-2.26.patch b/gwhy-2.26.patch new file mode 100644 index 0000000..15a2576 --- /dev/null +++ b/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 + + diff --git a/gwhy-icon.png b/gwhy-icon.png new file mode 100644 index 0000000..9a1b76c Binary files /dev/null and b/gwhy-icon.png differ diff --git a/gwhy.desktop b/gwhy.desktop new file mode 100644 index 0000000..27f853a --- /dev/null +++ b/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; \ No newline at end of file diff --git a/jessie.desktop b/jessie.desktop new file mode 100644 index 0000000..239f37a --- /dev/null +++ b/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; diff --git a/min.mlw b/min.mlw new file mode 100644 index 0000000..ae72dea --- /dev/null +++ b/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@ } \ No newline at end of file diff --git a/min_why.why.result b/min_why.why.result new file mode 100644 index 0000000..04848f9 --- /dev/null +++ b/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) + diff --git a/patch_jessie_pvs b/patch_jessie_pvs new file mode 100755 index 0000000..3e4abca --- /dev/null +++ b/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 + diff --git a/rem.pvs b/rem.pvs new file mode 100644 index 0000000..4f126a6 --- /dev/null +++ b/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 + diff --git a/sources b/sources new file mode 100644 index 0000000..760ff1b --- /dev/null +++ b/sources @@ -0,0 +1,3 @@ +34d8772de3d68c15a3a12935d90a0d60 krakatoa.pdf +a7eb00d1f78e59221629604167eb3151 caduceus.ps +cbb3b109a37f968bea9ffa6e43e3b822 why-2.29.tar.gz diff --git a/why-2.28-Makefile.in.patch b/why-2.28-Makefile.in.patch new file mode 100644 index 0000000..128b4e9 --- /dev/null +++ b/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) diff --git a/why.spec b/why.spec new file mode 100644 index 0000000..1c62b01 --- /dev/null +++ b/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 - 2.29-2 +- Fix broken conditionals + +* Mon Jul 11 2011 Jerry James - 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 2.28-2.2 +- add ppc to excludearch, too. No pvs-sbcl available there + +* Wed Apr 13 2011 Karsten Hopp 2.28-2.1 +- add ppc64 to excludearch, no sbcl available there + +* Mon Feb 07 2011 Fedora Release Engineering - 2.28-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild + +* Fri Jan 21 2011 Richard W.M. Jones - 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 - 2.26-2 +- Bump and rebuild for OCaml 3.12. + +* Sat Oct 09 2010 David A. Wheeler + Mark Rader - 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 - 2.23-2 +- Rebuild to fix dependencies. + +* Fri Jan 08 2010 Alan Dunn - 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 - 2.17-5 +- Exclude sparc64 s390 s390x there is no ocaml there + +* Fri Aug 07 2009 Alan Dunn - 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 - 2.17-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild + +* Wed Feb 25 2009 Fedora Release Engineering - 2.17-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild + +* Wed Dec 24 2008 Alan Dunn 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 2.14-2.1 +- ExcludeArch ppc64 on Fedora 8 due to no ocaml. +* Fri Aug 1 2008 Alan Dunn 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 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 2.13-2 +- Added several patches: fixed Zenon output, completed fix of rename + of cpulimit -> why-cpulimit. +* Wed Jul 23 2008 Alan Dunn 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) +