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