14 changed files with 1071 additions and 1 deletions
--- a/.gitignore
+++ b/.gitignore
@ -0,0 +1,3 @@
+/krakatoa.pdf
+/why-2.35.tar.gz
+/why-icons.tar.xz
--- a/README.why
+++ 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.
--- a/README.why-coq.Fedora
+++ 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.
--- a/dead.package
+++ b/dead.package
@ -1 +0,0 @@
-Abandoned by upstream and fails to build from source
--- a/div.pvs
+++ 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
+
--- a/jessie.appdata.xml
+++ b/jessie.appdata.xml
@ -0,0 +1,43 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<component type="desktop">
+ <id>jessie.desktop</id>
+ <metadata_license>CC0-1.0</metadata_license>
+ <project_license>LGPL-2.1</project_license>
+ <name>jessie</name>
+ <summary>Interface between why and Frama-C</summary>
+ <description>
+  <p>
+   Jessie is an interface between why and Frama-C.
+  </p>
+  <p>
+   Why is a software verification platform that applies formal proving tools to
+   annotated programs.  The Jessie plugin provide the ability to analyze C
+   programs by invoking Frama-C.
+  </p>
+ </description>
+ <screenshots>
+  <screenshot type="default">
+   <image>http://krakatoa.lri.fr/jessie/max_why3ide.png</image>
+   <caption>Interactive proof session</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png</image>
+   <caption>Max function proof</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/binary_search_raw.png</image>
+   <caption>Binary search function proof</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/binary_search_ovfl.png</image>
+   <caption>Binary search arithmetic overflow</caption>
+  </screenshot>
+  <screenshot>
+   <image>http://krakatoa.lri.fr/jessie/binary_search_behav.png</image>
+   <caption>Binar search function behavior</caption>
+  </screenshot>
+ </screenshots>
+ <update_contact>loganjerry@gmail.com</update_contact>
+ <url type="homepage">http://krakatoa.lri.fr/</url>
+ <url type="bugtracker">https://gforge.inria.fr/tracker/?atid=4012&amp;group_id=999&amp;func=browse</url>
+</component>
--- a/jessie.desktop
+++ b/jessie.desktop
@ -0,0 +1,7 @@
+[Desktop Entry]
+Name=jessie
+Comment=Verify C program using Jessie plug-in
+Exec=frama-c -jessie %F
+Icon=why
+Type=Application
+Categories=Development;
--- a/59
+++ b/59
@ -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
+
--- a/rem.pvs
+++ 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
+
--- a/3
+++ b/3
@ -0,0 +1,3 @@
+cc7a2e360acf8569a2eb878f51bfc8ff  krakatoa.pdf
+10bde72f95de8bc34135a8207cfcc9ec  why-2.35.tar.gz
+ed5648bbfb5e74fdfb814cdd725b191e  why-icons.tar.xz
--- a/why-2.35-Makefile.in.patch
+++ b/why-2.35-Makefile.in.patch
@ -0,0 +1,23 @@
+--- Makefile.in.orig	2015-03-25 08:32:17.000000000 -0600
+++ Makefile.in	2015-03-30 20:00:00.000000000 -0600
+@@ -815,17 +815,9 @@
+ 	mkdir -p $(LIBDIR)/why/coq7
+ 	cp -f $(VO7) $(LIBDIR)/why/coq7
+ install-coq-v8 install-coq-v8.1:
+-	if test -w $(COQLIB) ; then \
+-	  rm -f $(COQLIB)/user-contrib/Why*.v* ; \
+-	  rm -f $(COQLIB)/user-contrib/caduceus*.v* $(COQLIB)/user-contrib/Caduceus*.v* ; \
+-	  rm -f $(COQLIB)/user-contrib/jessie*.v* $(COQLIB)/user-contrib/Jessie*.v* ; \
+-	  mkdir -p $(COQLIB)/user-contrib/Why ; \
+-	  cp -f $(VO8) $(COQLIB)/user-contrib/Why ; \
+-	else \
+-	  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 -pf $(V8FILES) $(COQLIB)/user-contrib/Why
+	cp -pf $(VO8) $(COQLIB)/user-contrib/Why
+ 
+ install-pvs-no:
+ install-pvs-yes: $(PVSFILES)
--- a/why-frama-c-aluminium.patch
+++ b/why-frama-c-aluminium.patch
@ -0,0 +1,203 @@
+--- frama-c-plugin/interp.ml.orig	2015-03-25 08:32:17.000000000 -0600
+++ frama-c-plugin/interp.ml	2016-02-11 22:03:07.043502130 -0700
+@@ -2092,7 +2092,7 @@ let rec statement s =
+           effects of the statements... *)
+         JCPEblock(statement_list (List.map (fun (x,_,_,_,_) -> x) seq))
+ 
+-    | TryFinally _ | TryExcept _ -> assert false
+    | TryFinally _ | TryExcept _ | Throw _ | TryCatch _ -> assert false
+   in
+   (* Prefix statement by all non-case labels *)
+   let labels = filter_out is_case_label s.labels in
+@@ -2522,15 +2522,31 @@ let global vardefs g =
+ 
+     | GEnumTagDecl _ -> [] (* No enumeration declaration in Jessie *)
+ 
+-    | GVarDecl(_,v,pos) ->
+    | GVarDecl(v,_) ->
+         (* Keep only declarations for which there is no definition *)
+         if List.mem v vardefs
+-          || (isFunctionType v.vtype &&
+-                (v.vname = name_of_assert
+-                    || v.vname = name_of_free
+-                    || v.vname = name_of_malloc))
+         then []
+-        else if isFunctionType v.vtype then
+        else
+          [JCDvar(ctype v.vtype,v.vname,None)]
+
+    | GVar(v,{init=None},_pos) ->
+        [JCDvar(ctype v.vtype,v.vname,None)]
+
+    | GVar(_v,_iinfo,_pos) ->
+        (* Initialization should have been rewritten as code in an
+         * initialization function, that is called by the main function in
+         * global analyses and ignored otherwise.
+         *)
+        assert false
+
+    | GFunDecl(_,v,pos) ->
+        (* Keep only declarations for which there is no definition *)
+        if List.mem v vardefs
+          || v.vname = name_of_assert
+          || v.vname = name_of_free
+          || v.vname = name_of_malloc
+        then []
+        else
+           let rtyp = match unrollType v.vtype with
+             | TFun(rt,_,_,_) -> rt
+             | _ -> assert false
+@@ -2546,18 +2562,6 @@ let global vardefs g =
+           let formals = List.map formal params in
+           let s,_cba,_dba = spec v.vname funspec in
+           [JCDfun(ctype rtyp,id,formals,s,None)]
+-        else
+-          [JCDvar(ctype v.vtype,v.vname,None)]
+-
+-    | GVar(v,{init=None},_pos) ->
+-        [JCDvar(ctype v.vtype,v.vname,None)]
+-
+-    | GVar(_v,_iinfo,_pos) ->
+-        (* Initialization should have been rewritten as code in an
+-         * initialization function, that is called by the main function in
+-         * global analyses and ignored otherwise.
+-         *)
+-        assert false
+ 
+     | GFun(f,pos) ->
+         set_curFundec f;
+@@ -2692,7 +2696,9 @@ let file f =
+   in
+   let is_needed =
+     function
+-      | GVarDecl(_,v,_) when Cil.hasAttribute "FC_BUILTIN" v.vattr ->
+      | GVarDecl(v,_) when Cil.hasAttribute "FC_BUILTIN" v.vattr ->
+          v.vreferenced
+      | GFunDecl(_,v,_) when Cil.hasAttribute "FC_BUILTIN" v.vattr ->
+           v.vreferenced
+       | _ -> true
+   in
+--- frama-c-plugin/norm.ml.orig	2015-03-25 08:32:17.000000000 -0600
+++ frama-c-plugin/norm.ml	2016-06-01 17:46:29.597267704 -0600
+@@ -290,7 +290,7 @@ object(self)
+           attach_globaction (fun () -> Logic_utils.add_logic_function globinv);
+           ChangeTo [g;GAnnot(Dinvariant (globinv,v.vdecl),v.vdecl)]
+         else DoChildren
+-    | GVarDecl _ | GFun _ | GAnnot _ -> DoChildren
+    | GVarDecl _ | GFun _ | GFunDecl _ | GAnnot _ -> DoChildren
+     | GCompTag _ | GType _ | GCompTagDecl _ | GEnumTagDecl _
+     | GEnumTag _ | GAsm _ | GPragma _ | GText _ -> SkipChildren
+ 
+@@ -684,13 +684,13 @@ object(self)
+       fvi.vtype <- TFun(rt,params,isva,a)
+     in
+     function
+-      | GVarDecl(_spec,v,_attr) ->
+-          if isFunctionType v.vtype && not v.vdefined then retype_func v;
+      | GFunDecl(_spec,v,_attr) ->
+          if not v.vdefined then retype_func v;
+           DoChildren
+       | GFun _
+       | GAnnot _ -> DoChildren
+       | GVar _  | GCompTag _ | GType _ | GCompTagDecl _ | GEnumTagDecl _
+-      | GEnumTag _ | GAsm _ | GPragma _ | GText _ -> SkipChildren
+      | GVarDecl _ | GEnumTag _ | GAsm _ | GPragma _ | GText _ -> SkipChildren
+ 
+   method! vfunc f =
+     let var v =
+@@ -1015,7 +1015,7 @@ object(self)
+           | _ -> assert false
+         in
+         ChangeDoChildrenPost ([g], postaction)
+-    | GVarDecl _ | GFun _ | GAnnot _ -> DoChildren
+    | GVarDecl _ | GFun _ | GFunDecl _ | GAnnot _ -> DoChildren
+     | GCompTag _ | GType _ | GCompTagDecl _ | GEnumTagDecl _
+     | GEnumTag _ | GAsm _ | GPragma _ | GText _ -> SkipChildren
+ 
+@@ -1239,12 +1239,12 @@ object
+ *)
+           end;
+         SkipChildren
+-    | GVarDecl (_,v,_) ->
+    | GVarDecl (v,_) ->
+         (* No problem with calling [retype_var] more than once, since
+            subsequent calls do nothing on reference type. *)
+-        if not (isFunctionType v.vtype || v.vdefined) then retype_var v;
+        if not v.vdefined then retype_var v;
+         SkipChildren
+-    | GFun _ -> DoChildren
+    | GFun _ | GFunDecl _ -> DoChildren
+     | GAnnot _ -> DoChildren
+     | GCompTag(compinfo,_loc) ->
+         List.iter retype_field compinfo.cfields;
+@@ -1454,7 +1454,7 @@ object
+         in
+         List.iter field compinfo.cfields;
+         SkipChildren
+-    | GFun _ | GAnnot _ | GVar _ | GVarDecl _ -> DoChildren
+    | GFun _ | GFunDecl _ | GAnnot _ | GVar _ | GVarDecl _ -> DoChildren
+     | GType _ | GCompTagDecl _ | GEnumTagDecl _
+     | GEnumTag _ | GAsm _ | GPragma _ | GText _ -> SkipChildren
+ 
+@@ -1543,9 +1543,7 @@ object(self)
+       auto_type_wrappers :=
+         Cil_datatype.Typ.Set.add wrapper_type !auto_type_wrappers;
+       (* Treat newly constructed type *)
+-      let store_current_global = !currentGlobal in
+       ignore (Cil.visitCilGlobal (self:>Cil.cilVisitor) wrapper_def);
+-      currentGlobal := store_current_global;
+       (* Return the wrapper type *)
+       wrapper_type
+ 
+@@ -1674,10 +1672,10 @@ object(self)
+       | GFun (f, _) ->
+           retype_return f.svar;
+           DoChildren
+-      | GVarDecl (_, v, _) ->
+-          if isFunctionType v.vtype && not v.vdefined then
+-            retype_return v;
+      | GFunDecl (_, v, _) ->
+          if not v.vdefined then retype_return v;
+           DoChildren
+      | GVarDecl _
+       | GVar _
+       | GAnnot _ -> DoChildren
+       | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _
+@@ -1801,7 +1799,7 @@ object
+         let field fi = new_field_type fi in
+         let fty = List.map field fields in
+         ChangeTo (g::fty)
+-    | GFun _ | GAnnot _ | GVar _ | GVarDecl _ -> DoChildren
+    | GFun _ | GFunDecl _ | GAnnot _ | GVar _ | GVarDecl _ -> DoChildren
+     | GCompTag _ | GType _ | GCompTagDecl _ | GEnumTagDecl _
+     | GEnumTag _ | GAsm _ | GPragma _ | GText _ -> SkipChildren
+ 
+--- frama-c-plugin/rewrite.ml.orig	2015-03-25 08:32:17.000000000 -0600
+++ frama-c-plugin/rewrite.ml	2016-06-01 17:18:58.738619756 -0600
+@@ -56,7 +56,7 @@ class add_default_behavior =
+       then begin
+         let bhv = Cil.mk_behavior ~name:Cil.default_behavior_name () in
+         let kf = Extlib.the self#current_kf in
+-        let props = Property.ip_all_of_behavior kf Kglobal bhv in
+        let props = Property.ip_all_of_behavior kf Kglobal [] bhv in
+         List.iter Property_status.register props;
+         s.spec_behavior <- bhv :: s.spec_behavior
+       end;
+@@ -109,7 +109,7 @@ object
+     | GCompTagDecl(compinfo,_loc) ->
+ 	add_type (TComp(compinfo,empty_size_cache (),[]));
+ 	SkipChildren
+-    | GVarDecl _ | GVar _ | GFun _ | GAnnot _ | GType _
+    | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ | GAnnot _ | GType _
+     | GEnumTagDecl _ | GEnumTag _ | GAsm _ | GPragma _ | GText _ ->
+ 	DoChildren
+ 
+@@ -598,7 +598,7 @@ object
+                 in
+                  Cil.unsafeSetFormalsDecl f formals;
+                 my_globals <-
+-                  GVarDecl(Cil.empty_funspec(),f,loc) :: my_globals;
+                  GFunDecl(Cil.empty_funspec(),f,loc) :: my_globals;
+                 Globals.Functions.replace_by_declaration spec f loc;
+                 let kf = Globals.Functions.get f in
+                 Annotations.register_funspec ~emitter:Common.jessie_emitter kf;
--- a/why-ocamlgraph186.patch
+++ b/why-ocamlgraph186.patch
@ -0,0 +1,14 @@
+--- src/hypotheses_filtering.ml.orig	2015-03-25 08:32:17.000000000 -0600
+++ src/hypotheses_filtering.ml	2015-03-30 20:00:00.000000000 -0600
+@@ -1680,9 +1680,9 @@
+ *******************)
+ 
+ module W = struct 
+-  type label = PdlGraph.E.label
+  type edge = PdlGraph.E.t
+   type t = int
+-  let weight x = x
+  let weight e = PdlGraph.E.label e
+   let zero = 0
+   let add = (+)
+   let compare = compare
--- a/why.spec
+++ b/why.spec
@ -0,0 +1,632 @@
+# 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)
+
+Name:           why
+Version:        2.35
+Release:        18%{?dist}
+Summary:        Software verification platform
+
+License:        LGPLv2 with exceptions
+URL:            http://why.lri.fr/
+Source0:        http://why.lri.fr/download/%{name}-%{version}.tar.gz
+Source1:        http://krakatoa.lri.fr/manual/krakatoa.pdf
+Source2:        README.why-coq.Fedora
+Source3:        README.why
+Source4:        jessie.desktop
+Source5:        jessie.appdata.xml
+Source6:        div.pvs
+Source7:        rem.pvs
+Source8:        patch_jessie_pvs
+# Created with gimp from official upstream icon
+Source9:        %{name}-icons.tar.xz
+
+# 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.
+Patch0:         %{name}-2.35-Makefile.in.patch
+
+# Adapt to ocamlgraph 1.8.6
+Patch1:         %{name}-ocamlgraph186.patch
+
+# Adapt to Frama-C Aluminium
+Patch2:         %{name}-frama-c-aluminium.patch
+
+BuildRequires:  auto-destdir
+BuildRequires:  desktop-file-utils
+BuildRequires:  emacs xemacs xemacs-packages-extra
+BuildRequires:  frama-c
+BuildRequires:  gappalib-coq
+BuildRequires:  ocaml
+BuildRequires:  ocaml-apron-devel
+BuildRequires:  ocaml-camlp4-devel
+BuildRequires:  ocaml-findlib
+BuildRequires:  ocaml-mlgmpidl-devel
+BuildRequires:  ocaml-ocamldoc
+BuildRequires:  ocaml-ocamlgraph-devel
+BuildRequires:  why3
+BuildRequires:  coq
+%if %{has_pvs}
+BuildRequires:  pvs
+%endif
+
+Requires:       hicolor-icon-theme
+Requires:       emacs-filesystem
+Requires:       xemacs-filesystem
+
+# Filter out bogus requires
+%global __requires_exclude ocaml\\\((Ast|Cc|Env|Error|Jc_ast|Jc_env|Loc|Logic|Logic_decl|Misc|Ptree|Types)\\\)
+
+%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, Z3, 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 jessie
+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
+
+%package coq
+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.
+
+%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
+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 all
+Summary:        Complete Why software verification platform suite
+Requires:       why%{?_isa} = %{version}-%{release}
+Requires:       why-jessie%{?_isa} = %{version}-%{release}
+Requires:       why-coq%{?_isa} = %{version}-%{release}
+%if %{has_pvs}
+Requires:       why-pvs-support%{?_isa} = %{version}-%{release}
+%endif
+Requires:       alt-ergo gappalib-coq z3 zenon
+
+%description all
+This package provides a complete software verification platform suite
+based on Why, including various automated and interactive provers.
+
+%prep
+%setup -q
+%setup -q -T -D -a 9
+%patch0
+%patch1
+%patch2
+
+cp -p %SOURCE2 ./
+
+# Link with Fedora LDFLAGS
+for flag in $RPM_LD_FLAGS; do
+  sed -e "\%^bin/jessie\.opt%,\%^bin/jessie\.byte%s|-o|-ccopt $flag &|" \
+      -e "/gtkThread\.cmx/s|-o|-ccopt $flag &|" \
+      -i Makefile.in
+done
+
+%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 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 rpath and adapt to newer versions of apron
+sed -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
+    -e "s|box\.cmxa polka.cmxa|boxMPQ.cmxa polkaMPQ.cmxa|" \
+    -i configure
+
+# Enable debuginfo
+sed -i 's,@STRIP@,/usr/bin/true,;s,-dtypes [^-],-g &,' Makefile.in
+sed -ri 's,ocaml(c|opt),& -g,' atp/Makefile
+
+# Command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
+sed -e 's/command = "pvs"/command = "pvs-sbcl"/' \
+    -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
+    -i tools/dpConfig.ml
+sed -i 's/pvs/pvs-sbcl/' configure
+
+# Allow building with why3 0.87.2, Frama-C Aluminium, and flocq 2.5.1
+sed -e 's/0\.85|0\.86/&|0.87.2/' \
+    -e 's/Sodium-20150201/Aluminium-20160501/;s/Sodium/Aluminium/' \
+    -e 's/FRAMAC -version.*`/FRAMAC -version`/' \
+    -e 's/Import Flocq_version/Import Flocq.Flocq_version/' \
+    -i configure
+
+# Fix detection of why3
+sed -i '/WHY3/s/\\+\\) \.\*/*\\).*/' 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
+
+%configure --enable-apron --enable-verbosemake
+make %{opt_option}
+
+%install
+# Avoid a bug in PVS batch mode when using emacs
+make install DESTDIR=%{buildroot} %{opt_option} \
+     PVSLIB=%{buildroot}%{_libdir}/pvs/lib PVSEMACS=xemacs
+
+# Fix permissions
+chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/META.frama-c-jessie
+chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/Jessie.cmi
+chmod a-x %{buildroot}%{_libdir}/frama-c/plugins/top/Jessie.cm{a,o,x}
+
+# If no PVS, no .pvs files should be installed
+%if ! %{has_pvs}
+rm -fr %{buildroot}%{_libdir}/pvs
+%endif
+
+# Install desktop file
+desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE4}
+
+# Install AppData files
+mkdir -p %{buildroot}%{_datadir}/appdata
+install -pm 644 %{SOURCE5} %{buildroot}%{_datadir}/appdata
+
+# Install the icons
+mkdir -p %{buildroot}%{_datadir}/icons
+cp -a icons %{buildroot}%{_datadir}/icons/hicolor
+
+%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 %{SOURCE6} %{SOURCE7} %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p %{SOURCE8}            %{buildroot}%{_bindir}/
+%endif
+
+%global why_doc_dir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/%{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 %{SOURCE1} %{SOURCE3} CHANGES 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
+make check
+
+%post jessie
+update-desktop-database &> /dev/null || :
+touch --no-create %{_datadir}/icons/hicolor &>/dev/null
+gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
+
+%postun jessie
+update-desktop-database &> /dev/null || :
+touch --no-create %{_datadir}/icons/hicolor &>/dev/null
+gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || :
+
+%files
+%license COPYING LICENSE
+%{_bindir}/*
+%{_libdir}/why/
+%{_datadir}/icons/hicolor/*/apps/%{name}.png
+%{_emacs_sitelispdir}/why.el*
+%{_xemacs_sitelispdir}/why.el*
+%{why_doc_dir}/
+# This last example is really an example only for Coq - only .v files
+%exclude %{why_examples_dir}mlw/string-matching/
+# why-jessie
+%exclude %{_bindir}/jessie
+# why-pvs-support:
+%exclude %{_bindir}/patch_jessie_pvs
+
+%files jessie
+%{_bindir}/jessie
+%{_libdir}/frama-c/plugins/Jessie.cmi
+%{_libdir}/frama-c/plugins/META.frama-c-jessie
+%{_libdir}/frama-c/plugins/top/Jessie.*
+%{_datadir}/appdata/jessie.appdata.xml
+%{_datadir}/applications/jessie.desktop
+
+%files coq
+%doc README.why-coq.Fedora
+%{_libdir}/coq/user-contrib/Why/
+
+%if %{has_pvs}
+%files pvs-support
+%{_libdir}/pvs/lib/*
+%{_bindir}/patch_jessie_pvs
+%endif
+
+# "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
+* Fri Sep  2 2016 Jerry James <loganjerry@gmail.com> - 2.35-18
+- Rebuild for why3 0.87.2
+
+* Fri Jul 22 2016 Jerry James <loganjerry@gmail.com> - 2.35-17
+- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0
+
+* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 2.35-16
+- Rebuild for coq 8.5pl2
+
+* Wed Jun  1 2016 Jerry James <loganjerry@gmail.com> - 2.35-15
+- Rebuild for why3 0.87.1 and Frama-C Aluminium
+
+* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 2.35-14
+- Rebuild for coq 8.5pl1
+
+* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 2.35-13
+- Rebuild for ocaml-ocamlgraph 1.8.7
+
+* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 2.35-12
+- Rebuild for why3 0.87.0
+
+* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 2.35-11
+- Rebuild for coq 8.5, flocq 2.5.1, gappalib-coq 1.2.1, why3 0.86.3, and
+  Frama-C Magnesium
+- Use camlp4 in preference to camlp5
+- Drop cvc3 support
+- Update appdata for latest specification
+
+* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 2.35-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 2.35-9
+- Rebuild for flocq 2.5.0, gappalib-coq 1.2.0, and why3 0.86.2
+
+* Thu Jul 30 2015 Richard W.M. Jones <rjones@redhat.com> - 2.35-8
+- OCaml 4.02.3 rebuild.
+
+* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 2.35-7
+- Rebuild for why3 0.86.1
+
+* Fri Jun 19 2015 Richard W.M. Jones <rjones@redhat.com> - 2.35-6
+- Rebuild for ocaml-4.02.2.
+
+* Fri Jun 19 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.35-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
+
+* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 2.35-4
+- Rebuild for why3 0.86
+
+* Mon Apr 13 2015 Jerry James <loganjerry@gmail.com> - 2.35-3
+- Rebuild for coq 8.4pl6
+
+* Wed Apr  1 2015 Jerry James <loganjerry@gmail.com> - 2.35-2
+- Adjust requires filter
+
+* Tue Mar 31 2015 Jerry James <loganjerry@gmail.com> - 2.35-1
+- New upstream release
+- Drop upstreamed -flocq24 and -frama-c-sodium patches
+- Drop all gwhy-related sources, as gwhy has been retired
+- Merge (X)Emacs files into the main package due to change in policy
+
+* Thu Mar 19 2015 Jerry James <loganjerry@gmail.com> - 2.34-18
+- Rebuild for Frama-C Sodium
+- Add -ocamlgraph186 patch to adapt to ocamlgraph 1.8.6
+- Add -frama-c-sodium patch to adapt to Frama-C Sodium
+
+* Thu Feb 19 2015 Richard W.M. Jones <rjones@redhat.com> - 2.34-17
+- ocaml-4.02.1 rebuild.
+
+* Sat Nov 15 2014 Jerry James <loganjerry@gmail.com> - 2.34-16
+- Fix gwhy-2.33.patch (bz 1164470)
+
+* Thu Nov 13 2014 Richard W.M. Jones <rjones@redhat.com> - 2.34-15
+- Bump and rebuild for broken dependencies.
+
+* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 2.34-14
+- Rebuild for coq 8.4pl5
+
+* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-13
+- Rebuild for why3 0.85
+
+* Mon Sep  8 2014 Jerry James <loganjerry@gmail.com> - 2.34-12
+- Rebuild for fixed frama-c
+- Fix license handling
+
+* Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 2.34-11
+- Rebuild for the final ocaml 4.02.0 release
+
+* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 2.34-10
+- ocaml-4.02.0+rc1 rebuild.
+
+* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.34-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
+
+* Mon Aug  4 2014 Jerry James <loganjerry@gmail.com> - 2.34-8
+- OCaml 4.02.0 beta rebuild
+- BR emacs instead of emacs-nox, which no longer exists
+
+* Tue Jun 24 2014 Jerry James <loganjerry@gmail.com> - 2.34-7
+- Omit "-z now" when building with relro (bz 1105265)
+- Resolve a conflict between Frama-C and why modules both named "Project"
+
+* Sun Jun 08 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.34-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
+
+* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 2.34-5
+- Rebuild for coq 8.4pl4
+
+* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 2.34-4
+- Rebuild for ocamlgraph 1.8.5 and flocq 2.3.0
+- Drop has_coq macro, since coq is now universally available
+- Add -flocq23 patch to adapt to flocq 2.3.0
+
+* Tue Apr 15 2014 Richard W.M. Jones <rjones@redhat.com> - 2.34-3
+- Remove ocaml_arches macro (RHBZ#1087794).
+
+* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 2.34-2
+- Remove dropped patches
+- Add icons
+- Fix the desktop icon entries
+
+* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 2.34-1
+- New upstream release
+- Drop upstreamed -hashtbl, -flocq, and -or patches
+- Add ocaml-findlib BR
+
+* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 2.33-6
+- Rebuild for ocamlgraph 1.8.4
+- Update desktop files
+- Add AppData files for gwhy and jessie
+
+* Tue Sep 17 2013 Jerry James <loganjerry@gmail.com> - 2.33-5
+- Rebuild for OCaml 4.01.0
+- Enable debuginfo
+- Add -or patch to fix warnings, since warnings are errors
+
+* Sat Jul 27 2013 Ville Skyttä <ville.skytta@iki.fi> - 2.33-4
+- Install docs to %%{_pkgdocdir} where available.
+
+* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 2.33-3
+- Rebuild for frama-c Fluorine 20130601
+
+* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 2.33-2
+- Rebuild for new frama-c and why3 builds
+
+* Tue May 14 2013 Jerry James <loganjerry@gmail.com> - 2.33-1
+- New upstream release
+- Drop upstreamed -warning, -coq84, and -ocaml4 patches
+- Add -hashtbl patch
+- Enable Jessie plugin again
+
+* Sat Feb 09 2013 Parag Nemade <paragn AT fedoraproject DOT org> - 2.31-7
+- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077
+
+* Mon Jan 14 2013 Jerry James <loganjerry@gmail.com> - 2.31-6
+- Rebuild for alt-ergo 0.95
+
+* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 2.31-5
+- Rebuild for coq 8.4pl1
+
+* Fri Oct 19 2012 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 2.31-3
+- Rebuild for new frama-c build with altered API.
+
+* Mon Aug 27 2012 Jerry James <loganjerry@gmail.com> - 2.31-2
+- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning
+
+* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 2.30-7
+- Rebuild for OCaml 4.00.0 official.
+
+* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.30-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
+
+* Wed Jan 11 2012 Jerry James <loganjerry@gmail.com> - 2.30-5
+- Patch to work with flocq 2.0.0
+
+* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 2.30-4
+- Rebuild for coq 8.3pl3
+
+* Tue Dec  6 2011 Jerry James <loganjerry@gmail.com> - 2.30-3
+- Update alt_ergo and yices "okay" version numbers
+
+* Wed Nov 23 2011 Jerry James <loganjerry@gmail.com> - 2.30-2
+- Rebuild with APRON and gappalib-coq support
+
+* Fri Oct 28 2011 Jerry James <loganjerry@gmail.com> - 2.30-1
+- New upstream release
+
+* 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.
				`@ -1 +0,0 @@`
				`Abandoned by upstream and fails to build from source`