diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ba8b107 --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +/krakatoa.pdf +/why-icons.tar.xz +/why-2.36.tar.gz +/why-2.38.tar.gz +/why-2.39.tar.gz 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/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/jessie.appdata.xml b/jessie.appdata.xml new file mode 100644 index 0000000..3cbd299 --- /dev/null +++ b/jessie.appdata.xml @@ -0,0 +1,43 @@ + + + jessie.desktop + CC0-1.0 + LGPL-2.1 + jessie + Interface between why and Frama-C + +

+ Jessie is an interface between why and Frama-C. +

+

+ 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. +

+ + + + http://krakatoa.lri.fr/jessie/max_why3ide.png + Interactive proof session + + + http://krakatoa.lri.fr/jessie/max_ptr_why3ide.png + Max function proof + + + http://krakatoa.lri.fr/jessie/binary_search_raw.png + Binary search function proof + + + http://krakatoa.lri.fr/jessie/binary_search_ovfl.png + Binary search arithmetic overflow + + + http://krakatoa.lri.fr/jessie/binary_search_behav.png + Binar search function behavior + + + loganjerry@gmail.com + http://krakatoa.lri.fr/ + https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse + diff --git a/jessie.desktop b/jessie.desktop new file mode 100644 index 0000000..099b3ad --- /dev/null +++ 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; 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..77125d9 --- /dev/null +++ b/sources @@ -0,0 +1,3 @@ +SHA512 (krakatoa.pdf) = 5d0f4e6b938ddc1eafa48264c02cf99e68f776a7e190b997e35fb2cd154627b5d27369886f570cbcfdfe5f3a1929a97a1fec9457a6f6662f83cbb2e51f65ca04 +SHA512 (why-2.39.tar.gz) = b36e9423ff82fa2f51fea40a33021ed0def3719d9421b2f7f1e2aa1d6113faacf932984ac293b6d0ac92f800fd48efbdd8cc3ec6a929003a57da20efab682bad +SHA512 (why-icons.tar.xz) = d6ca78cf09540f5742564912470fb8c49f7d11ca16cd8bb60c8790af10c1591198f6020bd792cff8e3464f762b7ef0a690d3e4ba1a2cf670c286c8056d266bc3 diff --git a/why-project.patch b/why-project.patch new file mode 100644 index 0000000..e50186a --- /dev/null +++ b/why-project.patch @@ -0,0 +1,115 @@ +--- Makefile.in.orig 2017-08-23 02:08:38.000000000 -0600 ++++ Makefile.in 2017-12-04 21:00:24.549232019 -0700 +@@ -154,7 +154,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src + src/effect.cmo src/pp.cmo src/option_misc.cmo \ + src/report.cmo \ + src/explain.cmo \ +- src/xml.cmo src/project.cmo ++ src/xml.cmo src/whyproject.cmo + + # jessie + JCCML_EXPORT = src/why3_kw.ml jc/output.ml \ +--- src/options.mli.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/options.mli 2017-12-04 21:01:17.268996320 -0700 +@@ -184,7 +184,7 @@ val files : string list + (*s GUI? *) + + val gui : bool ref +-val gui_project : Project.t option ref ++val gui_project : Whyproject.t option ref + val lib_files_to_load : string list + + (* +--- src/pretty.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/pretty.ml 2017-12-04 21:02:42.540615229 -0700 +@@ -416,12 +416,12 @@ let output_project f = + with Not_found -> + functions := SMap.add fn SMap.empty !functions) + Util.program_locs ; +- let p = Project.create (Filename.basename f) in +- Project.set_project_context_file p (f ^ "_ctx.why"); ++ let p = Whyproject.create (Filename.basename f) in ++ Whyproject.set_project_context_file p (f ^ "_ctx.why"); + List.iter + (fun (expl,fpo) -> + let n = expl.lemma_or_fun_name in +- let _ = Project.add_lemma p n expl fpo in ()) ++ let _ = Whyproject.add_lemma p n expl fpo in ()) + !lemmas; + SMap.iter + (fun fname behs -> +@@ -431,15 +431,15 @@ let output_project f = + floc + with Not_found -> Loc.dummy_floc + in +- let f = Project.add_function p fname floc in ++ let f = Whyproject.add_function p fname floc in + SMap.iter + (fun beh vcs -> +- let be = Project.add_behavior f beh floc in ++ let be = Whyproject.add_behavior f beh floc in + List.iter + (fun (expl,fpo) -> +- let _ = Project.add_goal be expl fpo in ()) ++ let _ = Whyproject.add_goal be expl fpo in ()) + vcs) + behs) + !functions; +- Project.save p f; ++ Whyproject.save p f; + p +--- src/pretty.mli.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/pretty.mli 2017-12-04 21:03:05.635512035 -0700 +@@ -50,4 +50,4 @@ val output_files : string -> unit + (* [output_project f] produces a whole project description, in a file + [f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why], + and each goal in a separate file [f_po.why] for i=1,2,... *) +-val output_project : string -> Project.t ++val output_project : string -> Whyproject.t +--- src/whyweb.ml.orig 2017-08-23 02:08:38.000000000 -0600 ++++ src/whyweb.ml 2017-12-04 21:04:16.932193463 -0700 +@@ -29,7 +29,7 @@ + (**************************************************************************) + + open Format +-open Project ++open Whyproject + + (*prover*) + let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3] +@@ -168,7 +168,7 @@ let file = match !file with + | None -> () + | Some f -> Arg.usage spec usage; exit 1 + +-let proj = ref (Project.create "") ++let proj = ref (Whyproject.create "") + + let proj_file = ref "" + +@@ -260,7 +260,7 @@ let interp_com c = + let _ = Thread.create (launch_behavior Cvc3) b in () + | `LaunchCvc3Function f -> + let _ = Thread.create (launch_function Cvc3) f in () +- | `Save -> Project.save !proj !proj.project_name ++ | `Save -> Whyproject.save !proj !proj.project_name + end; + loc + with Not_found -> ("",0,0,0) +@@ -343,7 +343,7 @@ let main_page msg = + let load_prj file = + eprintf "Reading file %s@." file; + try +- proj := Project.load file; ++ proj := Whyproject.load file; + proj_file := file; + with + Sys_error _ -> +@@ -526,7 +526,7 @@ wprint "
Save Proj + " ns; + wprint ""; + List.iter (fun prover -> +- wprint "" (Project.provers_name prover)) ++ wprint "" (Whyproject.provers_name prover)) + provers; + wprint " + "; diff --git a/why.spec b/why.spec new file mode 100644 index 0000000..cf74d92 --- /dev/null +++ b/why.spec @@ -0,0 +1,599 @@ +# 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.39 +Release: 3%{?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 +# Avoid a clash between Frama-C and why modules both named "Project". +# Sent upstream 26 Jun 2014. +Patch0: %{name}-project.patch + +BuildRequires: auto-destdir +BuildRequires: desktop-file-utils +BuildRequires: 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: ocaml-zarith-devel +BuildRequires: why3 +BuildRequires: coq +%if %{has_pvs} +BuildRequires: pvs +%endif + +Requires: gappalib-coq +Requires: hicolor-icon-theme +Requires: emacs-filesystem + +# This can be removed once Fedora 25 reaches EOL +Obsoletes: %{name}-coq < 2.36-1 +Provides: %{name}-coq = %{version}-%{release} + +# 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 + +%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} +%if %{has_pvs} +Requires: why-pvs-support%{?_isa} = %{version}-%{release} +%endif +Requires: alt-ergo 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 + +# The other part of avoiding the "Project" module name clash +mv src/project.ml src/whyproject.ml +mv src/project.mli src/whyproject.mli + +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; do + %fix_encoding $f ISO-8859-1 UTF-8 +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 octMPQ.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 -i 's/pvs/pvs-sbcl/' configure + +# Allow building with OCaml 4.05 +sed -i 's/4\.04\.\*/4.04.*|4.05.*/' configure + +%build +%if ! %{opt} +%global opt_option OCAMLBEST=byte OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex +%else +%global opt_option OCAMLBEST=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}} + +# Fix up documentation and examples +mkdir -p %{buildroot}%{why_doc_dir} +cp -p %{SOURCE1} %{SOURCE3} CHANGES README Version %{buildroot}%{why_doc_dir} + +%check +make check + +%post jessie +touch --no-create %{_datadir}/icons/hicolor &>/dev/null +gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : + +%postun jessie +touch --no-create %{_datadir}/icons/hicolor &>/dev/null +gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : + +%files +%doc README.why-coq.Fedora +%license COPYING LICENSE +%{_bindir}/* +%{_libdir}/why/ +%{_datadir}/icons/hicolor/*/apps/%{name}.png +%{why_doc_dir}/ +# 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 + +%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 +* Sat Dec 9 2017 Jerry James - 2.39-3 +- Bring back the -project patch, still needed (bz 1520483) + +* Sat Oct 7 2017 Jerry James - 2.39-2 +- Rebuild for why3 0.88.0 + +* Thu Sep 7 2017 Jerry James - 2.39-1 +- New upstream release + +* Wed Sep 06 2017 Richard W.M. Jones - 2.39-1 +- Update to 2.39. + +* Wed Sep 06 2017 Richard W.M. Jones - 2.38-6 +- OCaml 4.05.0 rebuild. + +* Thu Aug 03 2017 Fedora Release Engineering - 2.38-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild + +* Thu Jul 27 2017 Fedora Release Engineering - 2.38-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild + +* Sat Jul 01 2017 Richard W.M. Jones - 2.38-3 +- Rebuild for OCaml 4.04.2. + +* Mon May 15 2017 Richard W.M. Jones - 2.38-2 +- Rebuild for OCaml 4.04.1. + +* Fri Mar 24 2017 Jerry James - 2.38-1 +- New upstream release + +* Sat Feb 11 2017 Fedora Release Engineering - 2.36-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild + +* Thu Jan 12 2017 Jerry James - 2.36-1 +- New upstream release + +* Wed Nov 30 2016 Jerry James - 2.35-23 +- Rebuild for gappalib-coq 1.3.2 + +* Sun Nov 06 2016 Richard W.M. Jones - 2.35-21 +- Rebuild for OCaml 4.04.0. +- Modify configure script to allow building with OCaml 4.04. +- Modify configure script to use octMPQ library (part of Apron). + +* Fri Oct 28 2016 Jerry James - 2.35-20 +- Rebuild for coq 8.5pl3 +- Remove obsolete scriptlets + +* Thu Sep 29 2016 Jerry James - 2.35-19 +- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1 + +* Fri Sep 2 2016 Jerry James - 2.35-18 +- Rebuild for why3 0.87.2 + +* Fri Jul 22 2016 Jerry James - 2.35-17 +- Rebuild for apron 0.9.11 and gappalib-coq 1.3.0 + +* Wed Jul 13 2016 Jerry James - 2.35-16 +- Rebuild for coq 8.5pl2 + +* Wed Jun 1 2016 Jerry James - 2.35-15 +- Rebuild for why3 0.87.1 and Frama-C Aluminium + +* Fri Apr 22 2016 Jerry James - 2.35-14 +- Rebuild for coq 8.5pl1 + +* Sat Apr 16 2016 Jerry James - 2.35-13 +- Rebuild for ocaml-ocamlgraph 1.8.7 + +* Fri Mar 18 2016 Jerry James - 2.35-12 +- Rebuild for why3 0.87.0 + +* Fri Feb 12 2016 Jerry James - 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 - 2.35-10 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild + +* Wed Oct 14 2015 Jerry James - 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 - 2.35-8 +- OCaml 4.02.3 rebuild. + +* Mon Jun 22 2015 Jerry James - 2.35-7 +- Rebuild for why3 0.86.1 + +* Fri Jun 19 2015 Richard W.M. Jones - 2.35-6 +- Rebuild for ocaml-4.02.2. + +* Fri Jun 19 2015 Fedora Release Engineering - 2.35-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild + +* Sat May 16 2015 Jerry James - 2.35-4 +- Rebuild for why3 0.86 + +* Mon Apr 13 2015 Jerry James - 2.35-3 +- Rebuild for coq 8.4pl6 + +* Wed Apr 1 2015 Jerry James - 2.35-2 +- Adjust requires filter + +* Tue Mar 31 2015 Jerry James - 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 - 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 - 2.34-17 +- ocaml-4.02.1 rebuild. + +* Sat Nov 15 2014 Jerry James - 2.34-16 +- Fix gwhy-2.33.patch (bz 1164470) + +* Thu Nov 13 2014 Richard W.M. Jones - 2.34-15 +- Bump and rebuild for broken dependencies. + +* Thu Oct 30 2014 Jerry James - 2.34-14 +- Rebuild for coq 8.4pl5 + +* Thu Sep 18 2014 Jerry James - 2.34-13 +- Rebuild for why3 0.85 + +* Mon Sep 8 2014 Jerry James - 2.34-12 +- Rebuild for fixed frama-c +- Fix license handling + +* Tue Sep 2 2014 Jerry James - 2.34-11 +- Rebuild for the final ocaml 4.02.0 release + +* Mon Aug 25 2014 Jerry James - 2.34-10 +- ocaml-4.02.0+rc1 rebuild. + +* Mon Aug 18 2014 Fedora Release Engineering - 2.34-9 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild + +* Mon Aug 4 2014 Jerry James - 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 - 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 - 2.34-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild + +* Tue May 13 2014 Jerry James - 2.34-5 +- Rebuild for coq 8.4pl4 + +* Mon Apr 21 2014 Jerry James - 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 - 2.34-3 +- Remove ocaml_arches macro (RHBZ#1087794). + +* Mon Mar 24 2014 Jerry James - 2.34-2 +- Remove dropped patches +- Add icons +- Fix the desktop icon entries + +* Tue Mar 18 2014 Jerry James - 2.34-1 +- New upstream release +- Drop upstreamed -hashtbl, -flocq, and -or patches +- Add ocaml-findlib BR + +* Wed Feb 26 2014 Jerry James - 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 - 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ä - 2.33-4 +- Install docs to %%{_pkgdocdir} where available. + +* Fri Jun 21 2013 Jerry James - 2.33-3 +- Rebuild for frama-c Fluorine 20130601 + +* Thu May 23 2013 Jerry James - 2.33-2 +- Rebuild for new frama-c and why3 builds + +* Tue May 14 2013 Jerry James - 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 - 2.31-7 +- Remove vendor tag from desktop file as per https://fedorahosted.org/fesco/ticket/1077 + +* 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.
%s%s