[why/f14/master] Update to version 2.26
David A. Wheeler
dwheeler at fedoraproject.org
Mon Oct 11 17:18:45 UTC 2010
commit a043f1ac0d4155c45a19d08064c06118402a5d33
Author: David A. Wheeler <dwheeler at dwheeler.com>
Date: Mon Oct 11 13:18:45 2010 -0400
Update to version 2.26
.gitignore | 2 +
div.pvs | 35 +++++
gwhy-2.23.patch => gwhy-2.26.patch | 0
jessie.desktop | 8 ++
patch_jessie_pvs | 59 +++++++++
rem.pvs | 35 +++++
sources | 2 +-
why-2.23-Makefile.in.patch | 49 -------
why-2.26-Makefile.in.patch | 22 ++++
why.spec | 245 +++++++++++++++++++++++-------------
10 files changed, 318 insertions(+), 139 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 7fd1d69..23521f0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
krakatoa.pdf
why-2.23.tar.gz
+/krakatoa.pdf
+/why-2.26.tar.gz
diff --git a/div.pvs b/div.pvs
new file mode 100644
index 0000000..4005fe3
--- /dev/null
+++ b/div.pvs
@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+%
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+%
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+%
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+div: THEORY
+BEGIN
+
+ x : VAR int
+ nzy : VAR nzint
+
+ div(x, nzy): int =
+ IF (x >= 0 AND nzy > 0) THEN ndiv(x, nzy)
+ ELSIF (x >= 0 AND nzy < 0) THEN -ndiv(x, -nzy)
+ ELSIF (x < 0 AND nzy > 0) THEN -ndiv(-x, nzy)
+ ELSE ndiv(-x, -nzy)
+ ENDIF
+
+END div
+
diff --git a/gwhy-2.23.patch b/gwhy-2.26.patch
similarity index 100%
rename from gwhy-2.23.patch
rename to gwhy-2.26.patch
diff --git a/jessie.desktop b/jessie.desktop
new file mode 100644
index 0000000..239f37a
--- /dev/null
+++ b/jessie.desktop
@@ -0,0 +1,8 @@
+[Desktop Entry]
+Encoding=UTF-8
+Name=jessie
+Comment=Verify C program using Jessie plug-in
+Exec=frama-c -jessie %f
+Icon=ICON-LOCATION-BASE/gwhy-icon.png
+Type=Application
+Categories=Development;
diff --git a/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
index debc831..d818982 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
14563361a9427e58115825b4e782d23e krakatoa.pdf
-8b8d8f6376e42c688521abf5d9f21a9c why-2.23.tar.gz
+ae10d920c6919aa30934e7383b260d6b why-2.26.tar.gz
diff --git a/why-2.26-Makefile.in.patch b/why-2.26-Makefile.in.patch
new file mode 100644
index 0000000..4d16144
--- /dev/null
+++ b/why-2.26-Makefile.in.patch
@@ -0,0 +1,22 @@
+--- why-2.23-old/Makefile.in 2010-01-04 21:08:49.858843630 -0500
++++ why-2.23/Makefile.in 2010-01-05 20:34:20.912391080 -0500
+ static:: $(STATICBINARY)
+@@ -842,15 +851,9 @@
+ cp -f $(V7FILES) $(LIBDIR)/why/coq7
+ cp -f $(VO7) $(LIBDIR)/why/coq7
+ install-coq-v8 install-coq-v8.1:
+- if test -w $(COQLIB) ; then \
+- mkdir -p $(COQLIB)/user-contrib ; \
+- cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
+- cp -f $(VO8) $(COQLIB)/user-contrib ; \
+- else \
+- echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
+- mkdir -p $(LIBDIR)/why/coq ;\
+- cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
+- fi
++ mkdir -p $(COQLIB)/user-contrib
++ cp -f $(V8FILES) $(COQLIB)/user-contrib
++ cp -f $(VO8) $(COQLIB)/user-contrib
+
+ install-pvs-no:
+ install-pvs-yes: $(PVSFILES)
diff --git a/why.spec b/why.spec
index 7c837af..4996a58 100644
--- a/why.spec
+++ b/why.spec
@@ -1,10 +1,10 @@
Name: why
-Version: 2.23
-Release: 2%{?dist}
-Summary: Why software verification platform
+Version: 2.26
+Release: 1%{?dist}
+Summary: Software verification platform
Group: Applications/Engineering
-License: GPLv2
+License: GPLv2 and MIT
URL: http://why.lri.fr/
Source0: http://why.lri.fr/download/why-%{version}.tar.gz
Source1: README.why-gwhy.Fedora
@@ -16,26 +16,40 @@ Source6: min.mlw
Source7: min_why.why.result
Source8: http://caduceus.lri.fr/manual/caduceus.ps
Source9: http://krakatoa.lri.fr/manual/krakatoa.pdf
+Source10: jessie.desktop
+Source11: div.pvs
+Source12: rem.pvs
+Source13: patch_jessie_pvs
# The gwhy execution shell script is not particularly informative
-# about when bad parameters are passed to it - this patch fixes that
+# 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-%{version}.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 is and their checking causes the rpm building to fail.
# It also makes a fix necessary to correctly build the bytecode only
# version of why by building the make_float_model tool correctly in
# this case.
Patch1: why-%{version}-Makefile.in.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
-BuildRequires: ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink
-BuildRequires: ocaml-ocamlgraph-devel
-BuildRequires: cvc3
+BuildRequires: ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel
+BuildRequires: ocaml-lablgtk-devel, ocaml-ocamlgraph-devel
+BuildRequires: desktop-file-utils, dos2unix, prelink
+BuildRequires: frama-c-devel >= 1.5
+BuildRequires: auto-destdir
+# Emacs is required for PVS to rebuild theories:
+BuildRequires: cvc3, pvs-sbcl, emacs
+
+# Specialized dependency generator used because of problems with the
+# default RPM OCAML dependency process. Per suggestion of the OCAML group:
+%define _use_internal_dependency_generator 0
+%define __find_requires /usr/lib/rpm/ocaml-find-requires.sh -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types -i Env -i Misc -i Cil_types -i Db_types -i Lattice_With_Isotropy -i Signature
+%define __find_provides /usr/lib/rpm/ocaml-find-provides.sh -i Project
+
ExcludeArch: sparc64 s390 s390x
%if 0%{?fedora} >= 11
@@ -69,6 +83,11 @@ work, Simplify, Alt-Ergo, Yices, Z3, CVC Lite, Zenon are supported and
Zenon is 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). Invoke the Jessie plug-in with:
+ frama-c -jessie FILE.c
+
+
%package gwhy
Group: Applications/Engineering
Summary: IDE for Why software verification platform
@@ -81,9 +100,9 @@ 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.
+
# No Coq for ppc64 -> certain subpackages can't be built, but main why can be
%if 0%{?has_coq} == 1
-
%package coq
Group: Applications/Engineering
Summary: Libraries for interfacing Coq with Why
@@ -93,8 +112,31 @@ BuildRequires: coq
%description coq
This package contains a set of routines that assist in the
manipulation of why Coq-formatted output within Coq.
+%endif
+
+# 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: why = %{version}
+%description pvs-support
+This package provides support definitions so that the Why software
+verification platform suite can invoke PVS without licensing issues.
+
+%package all
+Group: Applications/Engineering
+Summary: Complete Why software verification platform suite
+Requires: why = %{version}
+Requires: why-gwhy = %{version}
+%if 0%{?has_coq} == 1
+Requires: why-coq = %{version}
%endif
+Requires: alt-ergo cvc3 coq pvs-sbcl gappa
+%description all
+This package provides a complete software verification platform suite
+based on Why, including various automated and interactive provers.
%prep
%setup -q
@@ -102,44 +144,45 @@ manipulation of why Coq-formatted output within Coq.
%patch0 -p1
%patch1 -p1
-cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .
+cp -p %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 %SOURCE10 %SOURCE11 %SOURCE12 %SOURCE13 ./
+# Frama-C's makefile does not handle DESTDIR; this lets us override it:
+cp -p /usr/share/frama-c/Makefile.dynamic ./frama-c-plugin/
%build
-%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
-
-# Native ocaml builds do not seem to work on ppc64 (many packages have
-# this problem)
+# Native ocaml builds do not work on ppc64 (many packages have this problem)
%ifarch ppc64
%global opt 0
+%else
+%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%endif
-
-# It seems that we should not be creating debuginfo regardless of
-# whether we have opt or not, as debuginfo is not particularly useful
-# for OCaml programs
-
-# If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
-
-%global debug_package %{nil}
-
%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
+# Don't create debuginfo; it's not particularly useful for OCaml programs.
+%global debug_package %{nil}
-# We actually want to install library files into a non /usr/lib
-# directory as they aren't architecture dependent
+# This option prints the actual make commands so we can see what's
+# happening (eg: for debugging the spec file)
+%global why_make_options VERBOSEMAKE=yes %{opt_option}
-./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir} \
- %{!?has_coq: COQC=no}
-make %{opt_option}
+# Remove spurious error and warn if buggy 0.91 is used, per:
+# http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-October/002303.html
+sed -e 's/versions_ok = \["0\.91"\]/versions_ok = ["0.92.1"]/' -i tools/dpConfig.ml
+# 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 -e 's/pvs /pvs-sbcl /' -i configure
+# Must disable plug-ins that no longer work, else running will cause warnings.
+%configure --disable-security_slicing --disable-aorai PVSC=`which pvs-sbcl` %{!?has_coq: COQC=no}
+sed -e 's/\"\/usr\/share\/coq\"/\$(DESTDIR)\/usr\/share\/coq\//' -i Makefile
-# Remove unnecessary execstack permissions
-%if %opt
-execstack -c bin/*.opt bin/why-cpulimit
-%endif
-# Strip binaries (Makefile misses some of them, and don't want to add an extra patch)
+make %{why_make_options}
+
+# Strip binaries (the Makefile misses some of them)
strip bin/why-cpulimit
%if %opt
strip bin/*.opt
@@ -151,16 +194,20 @@ strip bin/*.opt
%else
%global why bin/why.byte
%endif
-export WHYLIB=lib
-%why --why --output min min.mlw
-unset WHYLIB
-diff min_why.why min_why.why.result > /dev/null
+WHYLIB=lib %why --why --output min.why min.mlw
+diff -u min.why min_why.why.result # Show differences from correct result.
%install
rm -rf %{buildroot}
+mkdir -p %{buildroot}%{_libdir} %{buildroot}%{_bindir} %{buildroot}%{_datadir}
-make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} \
- %{?has_coq: COQLIB=%{buildroot}%{_datadir}/coq} install
+#Edit makefile to use local Makefile.dynamic, and fix local version:
+sed -e 's/\$(FRAMAC_SHARE)\/Makefile.dynamic/.\/Makefile.dynamic/' -i ./frama-c-plugin/Makefile
+sed -e 's/echo/\# echo/' -i ./frama-c-plugin/Makefile.dynamic
+sed -e 's/>>/\# >>/' -i ./frama-c-plugin/Makefile.dynamic
+
+make-redir install DESTDIR=%{buildroot} %{why_make_options} PVSLIB=%{buildroot}%{_libdir}/pvs/lib
+sed -e 's!%{buildroot}!!' -i %{buildroot}%{_libdir}/pvs/lib/why/top.out
# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
%if 0%{?has_coq} != 1
@@ -168,25 +215,24 @@ rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
%endif
# Install desktop icon and menu entry
-
%global why_data_dir %{_datadir}/why
-%if %(test -d %{buildroot}%{why_data_dir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{why_data_dir}
-%endif
-cp gwhy-icon.png %{buildroot}%{why_data_dir}
-
-sed -i -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' gwhy.desktop
-
-desktop-file-install --vendor="fedora" \
---dir=%{buildroot}%{_datadir}/applications \
-gwhy.desktop
+cp -p gwhy-icon.png %{buildroot}%{why_data_dir}
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i gwhy.desktop
+desktop-file-install --vendor="fedora" \
+ --dir=%{buildroot}%{_datadir}/applications gwhy.desktop
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' -i jessie.desktop
+desktop-file-install --vendor="fedora" \
+ --dir=%{buildroot}%{_datadir}/applications jessie.desktop
+
+mkdir -p %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p div.pvs rem.pvs %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p patch_jessie_pvs %{buildroot}%{_bindir}/
%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
%global why_examples_dir %{why_doc_dir}examples/
-
%global fix_encoding() dos2unix %1; mv %1 %1.old; \
- iconv -f ISO-8859-1 -t UTF-8 < %1.old > %1; rm %1.old \
- %{nil}
+ iconv -f ISO-8859-1 -t UTF-8 < %1.old > %1; rm -f %1.old ;
# Fix up documentation and examples
mkdir -p %{buildroot}%{why_examples_dir}mlw/
@@ -199,47 +245,57 @@ cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE %{buildroot}%{why_doc_
# encodings, 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
+ mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
done
-for f in `find -regex '.*\(\.mlw\|\.why\)' | egrep -v '_inv|_coq|_why'`; do
-%fix_encoding $f
-cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
+for f in `find -regex '.*\(\.mlw\|\.why\)' | grep -E -v '_inv|_coq|_why'`; do
+ %fix_encoding $f
+ 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
+ mkdir -p %{buildroot}%{why_examples_dir}c/$d
done
for f in `find -regex '.*\.c'`; do
-%fix_encoding $f
-cp -p $f %{buildroot}%{why_examples_dir}c/$f
+ %fix_encoding $f
+ cp -p $f %{buildroot}%{why_examples_dir}c/$f
done
+
%clean
rm -rf %{buildroot}
+%post
+echo "ENABLE_JESSIE=yes" >> /usr/share/frama-c/known_plugins.ac
+semanage fcontext -a -t textrel_shlib_t '%{_libdir}/frama-c/plugins/Jessie.cmxs'
+restorecon '%{_libdir}/frama-c/plugins/Jessie.cmxs'
+
+%postun
+sed -e "/ENABLE_JESSIE=yes/d" -i /usr/share/frama-c/known_plugins.ac
+
%files
%defattr(-,root,root,-)
-# Binaries
%{_bindir}/*
-%exclude %{_bindir}/gwhy*
-# Data for programs
-%{why_data_dir}
-%exclude %{why_data_dir}/gwhy-icon.png
-%{_datadir}/caduceus
-%{_datadir}/jessie
-# % {_datadir}/krakatoa
-%exclude %{_datadir}/jessie/jc.cmo
-%if %opt
-%exclude %{_datadir}/jessie/jc.cmx
-%exclude %{_datadir}/jessie/jc.o
-%endif
-# Man page
+%{_libdir}/frama-c/*
+%{_libdir}/caduceus/*
+%{_libdir}/coq/*
+%{_libdir}/jessie/*
+%{_libdir}/why/*
+%{_libdir}/pvs/lib/why/
+%{_datadir}/coq/*
%{_mandir}/man1/why.1.gz
-# Documentation and examples
%{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*
+%exclude %{why_data_dir}/gwhy-icon.png
+# why-pvs-support:
+%exclude %{_bindir}/patch_jessie_pvs
+# why-coq:
+%exclude %{_datadir}/coq/user-contrib/*
+%exclude %{_libdir}/caduceus/coq/
+
%files gwhy
%defattr(-,root,root,-)
@@ -249,27 +305,33 @@ rm -rf %{buildroot}
%doc README.why-gwhy.Fedora
%{why_data_dir}/gwhy-icon.png
%{_datadir}/applications/fedora-gwhy.desktop
+%{_datadir}/applications/fedora-jessie.desktop
-%if 0%{?has_coq} == 1
+%if 0%{?has_coq} == 1
%files coq
%defattr(-,root,root,-)
-%dir %{_datadir}/coq
-%dir %{_datadir}/coq/user-contrib
-%{_datadir}/coq/user-contrib/Why*
-# % exclude % {_datadir}/coq/user-contrib/Why*.v
-%{_datadir}/coq/user-contrib/caduceus*
-# % exclude % {_datadir}/coq/user-contrib/caduceus*.v
-%{_datadir}/coq/user-contrib/Caduceus.v*
-# % exclude % {_datadir}/coq/user-contrib/Caduceus.v
-%{_datadir}/coq/user-contrib/jessie_why.v*
-# % exclude % {_datadir}/coq/user-contrib/jessie_why.v
-%{_datadir}/coq/jessie_why.v*
+%{_datadir}/coq/user-contrib/*
+%dir %{_libdir}/caduceus/coq/
%doc README.why-coq.Fedora
-
%endif
+%files pvs-support
+%defattr(-,root,root,-)
+%{_libdir}/pvs/lib/ints/
+%{_bindir}/patch_jessie_pvs
+
+
+# "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 Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler at 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 at gmail.com> - 2.23-2
- Rebuild to fix dependencies.
@@ -331,3 +393,8 @@ rm -rf %{buildroot}
of cpulimit -> why-cpulimit.
* Wed Jul 23 2008 Alan Dunn <amdunn at gmail.com> 2.13-1
- Initial Fedora RPM version.
+
+# TODO:
+# If file $HOME/.gwhyrc does not exist, autorun "why-config".
+# Finish packaging/integrating "APRON" (for Inference of annotations)
+
More information about the scm-commits
mailing list