[frama-c] Update -fixes patch to fix startup failures on ARM.

Jerry James jjames at fedoraproject.org
Fri Aug 9 21:30:53 UTC 2013


commit 9df8b1f5de325e4817d3de05fee12bcc3b06b2c4
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Fri Aug 9 15:30:33 2013 -0600

    Update -fixes patch to fix startup failures on ARM.

 frama-c-fixes.patch |   37 +++++++++++++++++++++++++++++++++++++
 frama-c.spec        |    5 ++++-
 2 files changed, 41 insertions(+), 1 deletions(-)
---
diff --git a/frama-c-fixes.patch b/frama-c-fixes.patch
index 512cacb..4bdb23c 100644
--- a/frama-c-fixes.patch
+++ b/frama-c-fixes.patch
@@ -48,3 +48,40 @@ Index: src/wp/LogicCompiler.ml
      (* Re-compile final cases *)
      let cases = List.map
        (fun (case,labels,types,lemma) -> 
+See http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003702.html.
+
+Index: external/unmarshal.ml
+===================================================================
+--- external/unmarshal.ml	(revision 23277)
++++ external/unmarshal.ml	(working copy)
+@@ -209,6 +209,8 @@
+ 
+ (* Auxiliary functions for handling closures. *)
+ 
++(* Not used by Frama-C, causing problems with ARM, see:
++http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003702.html
+ let (code_area_start, cksum) =
+   let s = Marshal.to_string id [Marshal.Closures] in
+   let cksum = String.sub s 0x1E 16 in
+@@ -222,6 +224,7 @@
+   let start = Obj.add_offset (Obj.field (Obj.repr id) 0) (Int32.neg ofs) in
+   (start, cksum)
+ ;;
++*)
+ 
+ let check_const ch s msg =
+   for i = 0 to String.length s - 1 do
+@@ -412,10 +415,12 @@
+           read_double_array stk t len readfloat_big
+ 
+       | 0x10 (* CODE_CODEPOINTER *) ->
++	assert false
++(* NOT USED BY Frama-C 
+           let ofs = getword ch in
+           check_const ch cksum "input_value: code mismatch";
+ 	  let offset_pointer = Obj.add_offset code_area_start ofs in
+-          return stk (do_transform t offset_pointer)
++          return stk (do_transform t offset_pointer) *)
+       | 0x11 (* CODE_INFIXPOINTER *) ->
+           let ofs = getword ch in
+           let clos = intern_rec [] t in
diff --git a/frama-c.spec b/frama-c.spec
index 2ded71a..f851a54 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -20,7 +20,7 @@
 
 Name:           frama-c
 Version:        1.9
-Release:        5%{?dist}
+Release:        6%{?dist}
 Summary:        Framework for source code analysis of C software
 
 Group:          Development/Libraries
@@ -234,6 +234,9 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
 %{_xemacs_sitelispdir}/acsl.el
 
 %changelog
+* Fri Aug  9 2013 Jerry James <loganjerry at gmail.com> - 1.9-6
+- Update -fixes patch to fix startup failures on ARM
+
 * Sat Aug 03 2013 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 1.9-5
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
 


More information about the scm-commits mailing list