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) -> 
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