diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
index 19e705f6..a244914c 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -1825,36 +1825,33 @@ object (self)
 
   method save_register
            (vmem: variable_t) (iaddr: ctxt_iaddress_t) (reg: register_t) =
-    if BCHCPURegisters.is_temporary_register reg then
-      ()
+    if self#env#is_stack_variable vmem then
+      TR.tfold
+        ~ok:(fun offset ->
+          match offset with
+          | ConstantOffset (n, NoOffset) ->
+             self#stackframe#add_register_spill ~offset:n#toInt reg iaddr
+          | _ ->
+             log_error_result
+               ~msg:"save_register:not a constant offset"
+               __FILE__ __LINE__
+               ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
+                (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)
+                ^ " and offset " ^ (memory_offset_to_string offset)])
+        ~error:(fun e ->
+          log_error_result
+            ~msg:"save_register"
+            __FILE__ __LINE__
+            (["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
+              (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e))
+        (self#env#get_memvar_offset vmem)
     else
-      if self#env#is_stack_variable vmem then
-        TR.tfold
-          ~ok:(fun offset ->
-            match offset with
-            | ConstantOffset (n, NoOffset) ->
-               self#stackframe#add_register_spill ~offset:n#toInt reg iaddr
-            | _ ->
-               log_error_result
-                 ~msg:"save_register:not a constant offset"
-                 __FILE__ __LINE__
-                 ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
-                  (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)
-                  ^ " and offset " ^ (memory_offset_to_string offset)])
-          ~error:(fun e ->
-            log_error_result
-              ~msg:"save_register"
-              __FILE__ __LINE__
-              (["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
-                (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e))
-          (self#env#get_memvar_offset vmem)
-      else
-        log_error_result
-          ~msg:"save register:not a stack variable"
-          __FILE__ __LINE__
-          ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
-           "not a stack variable: "
-           ^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)]
+      log_error_result
+        ~msg:"save register:not a stack variable"
+        __FILE__ __LINE__
+        ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
+         "not a stack variable: "
+         ^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)]
 
   method restore_register
            (memaddr: xpr_t) (iaddr:ctxt_iaddress_t) (reg:register_t) =
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml
index 01921aeb..4b0c0d35 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml
@@ -465,75 +465,81 @@ object (self)
 
   method add_register_spill
            ~(offset: int) (reg: register_t) (iaddr:ctxt_iaddress_t) =
-    let spill = RegisterSpill (offset, reg) in
-    begin
-      (if H.mem stackslots offset then
-        if (H.find stackslots offset)#is_spill then
-          ()
-        else
-          let sslot = H.find stackslots offset in
-          raise
-            (BCH_failure
-               (LBLOCK [
-                    STR "Add register spill at address ";
-                    STR iaddr;
-                    STR " for register ";
-                    STR (register_to_string reg);
-                    STR " at offset ";
-                    INT offset;
-                    STR " cannot be completed, because another stackslot ";
-                    STR "at this offset, with name: ";
-                    STR sslot#name;
-                    STR " already exists"]))
-      else
-        let ssrec = {
-            sslot_name = (register_to_string reg) ^ "_spill";
-            sslot_offset = offset;
-            sslot_btype = t_unknown;
-            sslot_spill = Some reg;
-            sslot_size = Some 4;
-            sslot_desc = Some "register spill"
-          } in
-        let sslot = new stackslot_t ssrec in
-        H.add stackslots offset sslot);
+    if BCHCPURegisters.is_temporary_register reg then
+      ()
+    else
+      let spill = RegisterSpill (offset, reg) in
+      begin
+        (if H.mem stackslots offset then
+           if (H.find stackslots offset)#is_spill then
+             ()
+           else
+             let sslot = H.find stackslots offset in
+             raise
+               (BCH_failure
+                  (LBLOCK [
+                       STR "Add register spill at address ";
+                       STR iaddr;
+                       STR " for register ";
+                       STR (register_to_string reg);
+                       STR " at offset ";
+                       INT offset;
+                       STR " cannot be completed, because another stackslot ";
+                       STR "at this offset, with name: ";
+                       STR sslot#name;
+                       STR " already exists"]))
+         else
+           let ssrec = {
+               sslot_name = (register_to_string reg) ^ "_spill";
+               sslot_offset = offset;
+               sslot_btype = t_unknown;
+               sslot_spill = Some reg;
+               sslot_size = Some 4;
+               sslot_desc = Some "register spill"
+             } in
+           let sslot = new stackslot_t ssrec in
+           H.add stackslots offset sslot);
         self#add_access offset iaddr spill
-    end
+      end
 
   method add_register_restore
            ~(offset: int) (reg: register_t) (iaddr: ctxt_iaddress_t) =
-    let restore = RegisterRestore (offset, reg) in
-    begin
-      (if H.mem stackslots offset then
-        if (H.find stackslots offset)#is_spill then
-          ()
-        else
-          let sslot = H.find stackslots offset in
-          raise
-            (BCH_failure
-               (LBLOCK [
-                    STR "Add register restore at address ";
-                    STR iaddr;
-                    STR " for register ";
-                    STR (register_to_string reg);
-                    STR " at offset ";
-                    INT offset;
-                    STR " cannot be completed, because another stackslot ";
-                    STR "at this offset, with name: ";
-                    STR sslot#name;
-                    STR " already exists"]))
-      else
-        let ssrec = {
-            sslot_name = (register_to_string reg) ^ "_spill";
-            sslot_offset = offset;
-            sslot_btype = t_unknown;
-            sslot_spill = Some reg;
-            sslot_size = Some 4;
-            sslot_desc = Some "register_spill"
-          } in
-        let sslot = new stackslot_t ssrec in
-        H.add stackslots offset sslot);
-      self#add_access offset iaddr restore
-    end
+    if BCHCPURegisters.is_temporary_register reg then
+      ()
+    else
+      let restore = RegisterRestore (offset, reg) in
+      begin
+        (if H.mem stackslots offset then
+           if (H.find stackslots offset)#is_spill then
+             ()
+           else
+             let sslot = H.find stackslots offset in
+             raise
+               (BCH_failure
+                  (LBLOCK [
+                       STR "Add register restore at address ";
+                       STR iaddr;
+                       STR " for register ";
+                       STR (register_to_string reg);
+                       STR " at offset ";
+                       INT offset;
+                       STR " cannot be completed, because another stackslot ";
+                       STR "at this offset, with name: ";
+                       STR sslot#name;
+                       STR " already exists"]))
+         else
+           let ssrec = {
+               sslot_name = (register_to_string reg) ^ "_spill";
+               sslot_offset = offset;
+               sslot_btype = t_unknown;
+               sslot_spill = Some reg;
+               sslot_size = Some 4;
+               sslot_desc = Some "register_spill"
+             } in
+           let sslot = new stackslot_t ssrec in
+           H.add stackslots offset sslot);
+        self#add_access offset iaddr restore
+      end
 
   method add_load
            ~(baseoffset:int)