[frama-c] Add -fixes patch to fix code generation for inductive definitions.

[Jerry James]

commit 7307230f553b61a24402d390c38b79a269d17ffe
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Mon Jun 3 12:03:16 2013 -0600

    Add -fixes patch to fix code generation for inductive definitions.

 frama-c-fixes.patch |   50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 frama-c.spec        |    8 +++++++-
 2 files changed, 57 insertions(+), 1 deletions(-)
---
diff --git a/frama-c-fixes.patch b/frama-c-fixes.patch
new file mode 100644
index 0000000..512cacb
--- /dev/null
+++ b/frama-c-fixes.patch
@@ -0,0 +1,50 @@
+See http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-May/003637.html
+and http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-May/003645.html.
+
+Index: src/wp/LogicCompiler.ml
+===================================================================
+--- src/wp/LogicCompiler.ml	(revision 22639)
++++ src/wp/LogicCompiler.ml	(working copy)
+@@ -606,16 +606,21 @@
+ 	 List.fold_left (heap_case labels_used) support s)
+       Heap.Map.empty cases in
+     (* Make signature with collected chunks *)
+-    let (parm,sigm) = Heap.Map.fold
+-      (fun chunk labels acc ->
+-	 let basename = Chunk.basename_of_chunk chunk in
+-	 let tau = Chunk.tau_of_chunk chunk in
+-	 LabelSet.fold
+-	   (fun label (parm,sigm) ->
+-	      let x = Lang.freshvar ~basename tau in
+-	      x :: parm , Sig_chunk(chunk,label) :: sigm
+-	   ) labels acc)
+-      support (parp,sigp) in
++    let (parm,sigm) = 
++      let frame = logic_frame l.l_var_info.lv_name l.l_tparams in
++      in_frame frame
++	(fun () -> 
++	   Heap.Map.fold
++	     (fun chunk labels acc ->
++		let basename = Chunk.basename_of_chunk chunk in
++		let tau = Chunk.tau_of_chunk chunk in
++		LabelSet.fold
++		  (fun label (parm,sigm) ->
++		     let x = Lang.freshvar ~basename tau in
++		     x :: parm , Sig_chunk(chunk,label) :: sigm
++		  ) labels acc)
++	     support (parp,sigp) 
++	) () in
+     (* Set global Signature *)
+     let lfun = ACSL l in
+     let ldef = {
+@@ -624,8 +629,9 @@
+       d_params = parm ;
+       d_cluster = cluster ;
+       d_definition = Logic Qed.Logic.Prop ;
+-    } in 
++    } in
+     Definitions.update_symbol ldef ;
++    Signature.update l (SIG sigm) ;
+     (* Re-compile final cases *)
+     let cases = List.map
+       (fun (case,labels,types,lemma) -> 
diff --git a/frama-c.spec b/frama-c.spec
index 01e11cb..4768ae6 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -20,7 +20,7 @@
 
 Name:           frama-c
 Version:        1.9
-Release:        2%{?dist}
+Release:        3%{?dist}
 Summary:        Framework for source code analysis of C software
 
 Group:          Development/Libraries
@@ -31,6 +31,8 @@ Source0:        http://frama-c.com/download/%{name}-%{pkgversion}.tar.gz
 Source1:        frama-c-1.6.licensing
 Source2:        %{name}-gui.desktop
 Source3:        acsl.el
+# Post-release fixes from upstream
+Patch0:         %{name}-fixes.patch
 
 BuildRequires:  alt-ergo
 BuildRequires:  coq
@@ -131,6 +133,7 @@ support.
 
 %prep
 %setup -q -n %{name}-%pkgversion
+%patch0
 
 # Fix encodings
 iconv -f iso-8859-1 -t utf8 man/frama-c.1 > man/frama-c.1.conv
@@ -231,6 +234,9 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
 %{_xemacs_sitelispdir}/acsl.el
 
 %changelog
+* Mon Jun  3 2013 Jerry James <loganjerry at gmail.com> - 1.9-3
+- Add -fixes patch to fix code generation for inductive definitions
+
 * Thu May 23 2013 Jerry James <loganjerry at gmail.com> - 1.9-2
 - Update to bugfix Fluorine release