[why] Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning.

Jerry James jjames at fedoraproject.org
Mon Aug 27 22:20:07 UTC 2012


commit 6a0dc3090eb51d30728b8bd69c5caf49b36db9ee
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Mon Aug 27 16:19:46 2012 -0600

    Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning.

 why-2.31-coq84.patch |   13 ++++++++++++-
 why.spec             |   11 +++++++----
 2 files changed, 19 insertions(+), 5 deletions(-)
---
diff --git a/why-2.31-coq84.patch b/why-2.31-coq84.patch
index cff6767..31171cf 100644
--- a/why-2.31-coq84.patch
+++ b/why-2.31-coq84.patch
@@ -1,5 +1,16 @@
+--- ./configure.orig	2012-07-19 12:33:10.000000000 -0600
++++ ./configure	2012-08-27 16:04:19.054123072 -0600
+@@ -2739,7 +2739,7 @@ $as_echo "$COQVERSION" >&6; }
+ 	WHYLIBCOQ=lib/coq
+ 	cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v
+ 	case $COQVERSION in
+-	8.1*|8.2*|8.3*|trunk)
++	8.1*|8.2*|8.3*|8.4*|trunk)
+ 	  JESSIELIBCOQ=lib/coq/jessie_why.vo
+ 	  cp -f lib/coq/WhyCoqDev.v lib/coq/WhyCoqCompat.v
+           # useful ??? [VP] Yes, the hack for making the output compliant with
 --- ./lib/coq/WhyTuples.v.orig	2012-07-19 12:33:10.000000000 -0600
-+++ ./lib/coq/WhyTuples.v	2012-08-23 11:58:18.246520358 -0600
++++ ./lib/coq/WhyTuples.v	2012-08-27 16:03:58.726126152 -0600
 @@ -20,11 +20,9 @@
  
  Definition tuple_1 (X:Set) := X.
diff --git a/why.spec b/why.spec
index c964198..b9cc311 100644
--- a/why.spec
+++ b/why.spec
@@ -20,7 +20,7 @@
 
 Name:           why
 Version:        2.31
-Release:        1%{?dist}
+Release:        2%{?dist}
 Summary:        Software verification platform
 
 Group:          Applications/Engineering
@@ -67,7 +67,7 @@ BuildRequires:  auto-destdir
 BuildRequires:  cvc3
 BuildRequires:  desktop-file-utils
 BuildRequires:  emacs-nox xemacs xemacs-packages-extra
-#BuildRequires:  frama-c-devel
+BuildRequires:  frama-c-devel
 BuildRequires:  gappalib-coq
 BuildRequires:  gtk2-devel
 BuildRequires:  ocaml
@@ -296,7 +296,7 @@ make %{opt_option}
 
 # Strip binaries (the Makefile misses some of them)
 strip bin/why-cpulimit
-#strip frama-c-plugin/Jessie.cmxs
+strip frama-c-plugin/Jessie.cmxs
 %if %opt
 strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \
       bin/why2html.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt
@@ -411,7 +411,7 @@ diff -u min.why min_why.why.result  # Show differences from correct result.
 %files jessie
 %{_bindir}/jessie
 %{_libdir}/jessie/
-#%%{_libdir}/frama-c/plugins/Jessie.*
+%{_libdir}/frama-c/plugins/Jessie.*
 %{_datadir}/applications/fedora-jessie.desktop
 
 %if %{has_coq}
@@ -444,6 +444,9 @@ diff -u min.why min_why.why.result  # Show differences from correct result.
 
 
 %changelog
+* Mon Aug 27 2012 Jerry James <loganjerry at gmail.com> - 2.31-2
+- Frama-c is fixed; rebuild with the Jessie plugin enabled and functioning
+
 * Thu Aug 23 2012 Jerry James <loganjerry at gmail.com> - 2.31-1
 - New upstream version
 - Drop upstreamed patches


More information about the scm-commits mailing list