diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 719a194..0000000 --- a/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -/krakatoa.pdf -/why-2.31.tar.gz diff --git a/README.why b/README.why deleted file mode 100644 index ba95dfa..0000000 --- a/README.why +++ /dev/null @@ -1,8 +0,0 @@ -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 deleted file mode 100644 index 406a7a9..0000000 --- a/README.why-coq.Fedora +++ /dev/null @@ -1,6 +0,0 @@ -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 deleted file mode 100644 index 3cc41b4..0000000 --- a/README.why-gwhy.Fedora +++ /dev/null @@ -1,6 +0,0 @@ -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 new file mode 100644 index 0000000..497866a --- /dev/null +++ b/dead.package @@ -0,0 +1 @@ +Abandoned by upstream and fails to build from source diff --git a/div.pvs b/div.pvs deleted file mode 100644 index 4005fe3..0000000 --- a/div.pvs +++ /dev/null @@ -1,35 +0,0 @@ -% 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.31.patch b/gwhy-2.31.patch deleted file mode 100644 index c131f48..0000000 --- a/gwhy-2.31.patch +++ /dev/null @@ -1,53 +0,0 @@ ---- bin/gwhy.sh.orig 2012-07-19 12:33:10.000000000 -0600 -+++ bin/gwhy.sh 2012-07-30 20:23:41.708914796 -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 -gen-only $1 || exit 1 -+ b=`basename $file .java` -+ krakatoa -gen-only $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 $file || 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 deleted file mode 100644 index 9a1b76c..0000000 Binary files a/gwhy-icon.png and /dev/null differ diff --git a/gwhy.desktop b/gwhy.desktop deleted file mode 100644 index 27f853a..0000000 --- a/gwhy.desktop +++ /dev/null @@ -1,8 +0,0 @@ -[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 deleted file mode 100644 index 239f37a..0000000 --- a/jessie.desktop +++ /dev/null @@ -1,8 +0,0 @@ -[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 deleted file mode 100644 index ae72dea..0000000 --- a/min.mlw +++ /dev/null @@ -1,4 +0,0 @@ -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 deleted file mode 100644 index 04848f9..0000000 --- a/min_why.why.result +++ /dev/null @@ -1,41 +0,0 @@ -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 deleted file mode 100755 index 3e4abca..0000000 --- a/patch_jessie_pvs +++ /dev/null @@ -1,59 +0,0 @@ -#!/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 deleted file mode 100644 index 4f126a6..0000000 --- a/rem.pvs +++ /dev/null @@ -1,35 +0,0 @@ -% 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 deleted file mode 100644 index c472a51..0000000 --- a/sources +++ /dev/null @@ -1,2 +0,0 @@ -08f92283da47fdb190f516339472e575 krakatoa.pdf -d647f64049345be5654f8f3fdb077aa4 why-2.31.tar.gz diff --git a/why-2.31-Makefile.in.patch b/why-2.31-Makefile.in.patch deleted file mode 100644 index 9546b4b..0000000 --- a/why-2.31-Makefile.in.patch +++ /dev/null @@ -1,20 +0,0 @@ ---- 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 @@ - mkdir -p $(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." ;\ -- fi -- mkdir -p $(LIBDIR)/why/coq -- cp -f $(VO8) $(LIBDIR)/why/coq -+ 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-2.31-coq84.patch b/why-2.31-coq84.patch deleted file mode 100644 index 31171cf..0000000 --- a/why-2.31-coq84.patch +++ /dev/null @@ -1,27 +0,0 @@ ---- ./configure.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./configure 2012-08-27 16:04:19.054123072 -0600 -@@ -2739,7 +2739,7 @@ $as_echo "$COQVERSION" >&6; } - WHYLIBCOQ=lib/coq - cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v - case $COQVERSION in -- 8.1*|8.2*|8.3*|trunk) -+ 8.1*|8.2*|8.3*|8.4*|trunk) - JESSIELIBCOQ=lib/coq/jessie_why.vo - cp -f lib/coq/WhyCoqDev.v lib/coq/WhyCoqCompat.v - # useful ??? [VP] Yes, the hack for making the output compliant with ---- ./lib/coq/WhyTuples.v.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./lib/coq/WhyTuples.v 2012-08-27 16:03:58.726126152 -0600 -@@ -20,11 +20,9 @@ - - Definition tuple_1 (X:Set) := X. - --Definition tuple_2 := prod. --Definition Build_tuple_2 := pair. -+Record tuple_2 (T1 T2:Set) : Set := -+ {proj_2_1 : T1; proj_2_2 : T2}. - Implicit Arguments Build_tuple_2. --Definition proj_2_1 := fst. --Definition proj_2_2 := snd. - - Record tuple_3 (T1 T2 T3:Set) : Set := - {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}. diff --git a/why-2.31-ocaml4.patch b/why-2.31-ocaml4.patch deleted file mode 100644 index 29e5e98..0000000 --- a/why-2.31-ocaml4.patch +++ /dev/null @@ -1,26 +0,0 @@ ---- ./jc/jc_stdlib_ge312.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./jc/jc_stdlib_ge312.ml 2012-07-31 15:26:24.760859244 -0600 -@@ -198,8 +198,9 @@ module Hashtbl = struct - - module type Std = sig - type ('a, 'b) t -- val create : int -> ('a, 'b) t -+ val create : ?random:bool -> int -> ('a, 'b) t - val clear : ('a, 'b) t -> unit -+ val reset : ('a, 'b) t -> unit - val add : ('a, 'b) t -> 'a -> 'b -> unit - val copy : ('a, 'b) t -> ('a, 'b) t - val find : ('a, 'b) t -> 'a -> 'b -@@ -210,8 +211,12 @@ module Hashtbl = struct - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c - val length : ('a, 'b) t -> int -+ val randomize : unit -> unit -+ val stats : ('a, 'b) t -> Hashtbl.statistics - val hash : 'a -> int -+ val seeded_hash : int -> 'a -> int - val hash_param : int -> int -> 'a -> int -+ val seeded_hash_param : int -> int -> int -> 'a -> int - end - - include (Hashtbl : Std) diff --git a/why-2.31-warning.patch b/why-2.31-warning.patch deleted file mode 100644 index 302748d..0000000 --- a/why-2.31-warning.patch +++ /dev/null @@ -1,88 +0,0 @@ ---- ./src/encoding_pred.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./src/encoding_pred.ml 2012-07-31 15:35:10.506221997 -0600 -@@ -266,11 +266,6 @@ let rec push d = - | Pnamed (s, p) -> - Pnamed (s, translate_eq p) - | p -> p in -- let rec lifted l p = -- match l with [] -> p -- | (_,a)::q -> -- lifted q (Forall(false, Ident.create a, Ident.create a, ut, [], p)) -- in - Queue.add (Dgoal - (loc, is_lemma, expl, name, - Env.empty_scheme ---- ./src/encoding_rec.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./src/encoding_rec.ml 2012-07-31 15:35:10.506221997 -0600 -@@ -397,11 +397,6 @@ let rec push d = - | Tconst (ConstUnit) as t -> plunge fv t PTunit - | Tconst (ConstFloat _) as t -> plunge fv t PTreal - | _ as t -> t in -- let rec lifted l p = -- match l with [] -> p -- | (_,a)::q -> -- lifted q (Forall(false, Ident.create a, Ident.create a, ut, [], p)) -- in - Queue.add (Dgoal - (loc, is_lemma, expl, name, - Env.empty_scheme ---- ./src/theoryreducer.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./src/theoryreducer.ml 2012-07-31 15:35:10.507222001 -0600 -@@ -191,11 +191,6 @@ struct - (** symbols the result **) - let symbolsSet = ref StringSet.empty in - let rec collect formula = -- let rec collectIntoAList l = match l with -- [] -> () -- | p :: r -> -- collect p ; -- collectIntoAList r in - match formula with - | Papp (id, [a; b], _) when is_eq id || is_neq id || id == t_zwf_zero-> - symbolsSet := StringSet.union (functionalSymbolsCollect a) ---- ./src/vcg.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./src/vcg.ml 2012-07-31 15:35:10.507222001 -0600 -@@ -615,13 +615,6 @@ let occur_as_var id = function - | Spred _ -> false - - let clean_sequent hyps concl = -- (* if a variable appears twice, we remove the first and its dependencies *) -- let rec filter_up_to x = function -- | [] -> [] -- | Svar (y, _) :: _ as hl when x = y -> hl -- | Spred (_, p) :: hl when occur_predicate x p -> filter_up_to x hl -- | h :: hl -> h :: filter_up_to x hl -- in - (* we remove variables not occuring at all in hypotheses or conclusion *) - let rec clean = function - | [] -> ---- ./src/theory_filtering.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./src/theory_filtering.ml 2012-07-31 15:35:10.507222001 -0600 -@@ -180,11 +180,6 @@ let symbols f = - (** symbols the result **) - let symbolsSet = ref Int_set.empty in - let rec collect formula = -- let rec collectIntoAList l = match l with -- [] -> () -- | p :: r -> -- collect p ; -- collectIntoAList r in - match formula with - | Papp (id, [a; b], _) when is_eq id || is_neq id || id == t_zwf_zero-> - symbolsSet := Int_set.union (functional_symbols a) ---- ./jc/jc_iterators.ml.orig 2012-07-19 12:33:10.000000000 -0600 -+++ ./jc/jc_iterators.ml 2012-07-31 15:35:52.481285428 -0600 -@@ -1057,13 +1057,6 @@ let replace_sub_expr e el = - | None -> None,el - | Some _ -> let e1,r = pop el in Some e1,r - in -- let rec popn n el = -- if n > 0 then -- let e,r = pop el in -- let el1,el2 = popn (n-1) r in -- e :: el1, el2 -- else [],el -- in - let enode = match e#node with - | JCEconst _ | JCEvar _ | JCEassert _ | JCEreturn_void as enode -> enode - | JCEcontract(req,dec,vi_result,behs,_e) -> diff --git a/why.spec b/why.spec deleted file mode 100644 index 5bddb95..0000000 --- a/why.spec +++ /dev/null @@ -1,591 +0,0 @@ -# Whether coq is available -%ifarch %{ocaml_arches} -%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.31 -Release: 6%{?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://krakatoa.lri.fr/manual/krakatoa.pdf -Source9: jessie.desktop -Source10: div.pvs -Source11: rem.pvs -Source12: 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.31.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: %{name}-2.31-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 - -BuildRequires: auto-destdir -BuildRequires: cvc3 -BuildRequires: desktop-file-utils -BuildRequires: emacs-nox xemacs xemacs-packages-extra -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-mlgmpidl-devel -BuildRequires: ocaml-ocamldoc -BuildRequires: ocaml-ocamlgraph-devel -BuildRequires: why3 -%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 "Frama-C"), 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: gappalib-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 gappalib-coq 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 -%patch2 -%patch3 -%patch4 - -cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./ - -# 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: add a missing include and a missing rpath -sed -e "s|-I +apron|-I +apron -I +gmp|" \ - -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";"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"]/' \ - -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-apron --enable-verbosemake -%else -%configure --enable-apron --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 -# Avoid a bug in PVS batch mode when using emacs -make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib \ - PVSEMACS=xemacs - -# 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 %{SOURCE5} %{buildroot}%{why_data_dir} -sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE4} > gwhy.desktop -desktop-file-install --vendor="fedora" \ - --dir=%{buildroot}%{_datadir}/applications gwhy.desktop -sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE9} > 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 %{SOURCE10} %{SOURCE11} %{buildroot}%{_libdir}/pvs/lib/ints/ -cp -p %{SOURCE12} %{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 %{SOURCE8} %{SOURCE3} 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}/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 - -%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/ -%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 -* Mon Jan 14 2013 Jerry James - 2.31-6 -- Rebuild for alt-ergo 0.95 - -* Mon Jan 7 2013 Jerry James - 2.31-5 -- Rebuild for coq 8.4pl1 - -* Fri Oct 19 2012 Jerry James - 2.31-4 -- Rebuild for OCaml 4.00.1 and frama-c Oxygen -- Recripple the Jessie plugin until it works with frama-c Oxygen - -* Tue Sep 11 2012 Jerry James - 2.31-3 -- Rebuild for new frama-c build with altered API. - -* Mon Aug 27 2012 Jerry James - 2.31-2 -- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning - -* Thu Aug 23 2012 Jerry James - 2.31-1 -- New upstream version -- Drop upstreamed patches -- Add ocaml-mlgmpidl-devel and why3 BRs -- Add -warning, -ocaml4, and -coq84 patches to fix the build -- Cripple the Jessie plugin until problems with frama-c and hashtables are fixed - -* Mon Jul 30 2012 Richard W.M. Jones - 2.30-7 -- Rebuild for OCaml 4.00.0 official. - -* Sun Jul 22 2012 Fedora Release Engineering - 2.30-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild - -* Wed Jan 11 2012 Jerry James - 2.30-5 -- Patch to work with flocq 2.0.0 - -* Tue Dec 27 2011 Jerry James - 2.30-4 -- Rebuild for coq 8.3pl3 - -* Tue Dec 6 2011 Jerry James - 2.30-3 -- Update alt_ergo and yices "okay" version numbers - -* Wed Nov 23 2011 Jerry James - 2.30-2 -- Rebuild with APRON and gappalib-coq support - -* Fri Oct 28 2011 Jerry James - 2.30-1 -- New upstream release - -* 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) -