diff --git a/CodeHawk/CH/chutil/cHTraceResult.ml b/CodeHawk/CH/chutil/cHTraceResult.ml
index 541faf5f..44e5146a 100644
--- a/CodeHawk/CH/chutil/cHTraceResult.ml
+++ b/CodeHawk/CH/chutil/cHTraceResult.ml
@@ -87,6 +87,19 @@ let tbind ?(msg="") (f: 'a -> 'c traceresult) (r: 'a traceresult) =
   | Error e -> Error (msg :: e)
 
 
+let tbind2
+      ?(msg1="")
+      ?(msg2="")
+      (f: 'a -> 'b -> 'c traceresult)
+      (r1: 'a traceresult)
+      (r2: 'b traceresult): 'c traceresult =
+  match r1, r2 with
+  | Ok v1, Ok v2 -> f v1 v2
+  | Error e1, Ok _ -> Error (msg1 :: e1)
+  | Ok _, Error e2 -> Error (msg2 :: e2)
+  | Error e1, Error e2 -> Error (msg1 :: msg2 :: (e1 @ e2))
+
+
 let tfold ~(ok:'a -> 'c) ~(error:string list -> 'c) (r: 'a traceresult): 'c =
   match r with
   | Ok v -> ok v
diff --git a/CodeHawk/CH/chutil/cHTraceResult.mli b/CodeHawk/CH/chutil/cHTraceResult.mli
index 26d0b22d..455a5110 100644
--- a/CodeHawk/CH/chutil/cHTraceResult.mli
+++ b/CodeHawk/CH/chutil/cHTraceResult.mli
@@ -100,6 +100,15 @@ val tbind:
   ?msg:string -> ('a -> 'c traceresult) -> ('a traceresult) -> 'c traceresult
 
 
+val tbind2:
+  ?msg1:string
+  -> ?msg2:string
+  -> ('a -> 'b -> 'c traceresult)
+  -> 'a traceresult
+  -> 'b traceresult
+  -> 'c traceresult
+
+
 (** [titer ~ok ~error r] is [ok v] if [r] is [Ok v] and [error e] if [r] is
     [Error e].*)
 val titer: ok:('a -> unit) -> error:(string list -> unit) -> ('a traceresult) -> unit
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
index e270de01..d4ef79ba 100644
--- a/CodeHawk/CHB/bchlib/bCHFloc.ml
+++ b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -89,16 +89,21 @@ module POAnchorCollections = CHCollections.Make
 let x2p = xpr_formatter#pr_expr
 let p2s = pretty_to_string
 let x2s x = p2s (x2p x)
+let i2s i = string_of_int i
 
 let opti2s (i: int option) =
   if Option.is_some i then string_of_int (Option.get i) else "?"
 
-let _ty2s (ty: btype_t) =
+let ty2s (ty: btype_t) =
   if is_unknown_type ty then "?" else btype_to_string ty
 let optty2s (ty: btype_t option) =
   if Option.is_some ty then btype_to_string (Option.get ty) else "?"
 
 
+let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line)
+let elocm (line: int): string = (eloc line) ^ ": "
+
+
 let log_error (tag: string) (msg: string): tracelogspec_t =
   mk_tracelog_spec ~tag:("floc:" ^ tag) msg
 
@@ -684,12 +689,11 @@ object (self)
            "memoff_r: "
            ^ (TR.tfold_default memory_offset_to_string "error" memoffset_r)] in
       TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+        ~msg:(eloc __LINE__)
         (fun memref ->
           if memref#is_global_reference then
             TR.tbind
-              ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)
-                    ^ ": memref:global")
+              ~msg:((elocm __LINE__) ^ ": memref:global")
               (fun memoff ->
                 TR.tbind
                   ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
@@ -698,10 +702,10 @@ object (self)
               memoffset_r
           else if memref#is_stack_reference then
             TR.tbind
-              ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:stack")
+              ~msg:((elocm __LINE__) ^ "memref:stack")
               (fun memoff ->
                 TR.tbind
-                  ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                  ~msg:(eloc __LINE__)
                   (fun numoff ->
                     if Option.is_some
                          (self#f#stackframe#containing_stackslot numoff#toInt) then
@@ -712,7 +716,7 @@ object (self)
               memoffset_r
           else
             TR.tmap
-              ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+              ~msg:(eloc __LINE__)
               (fun memoff ->
                 (self#env#mk_offset_memory_variable memref memoff))
               memoffset_r)
@@ -736,16 +740,15 @@ object (self)
       let address = simplify_xpr (inv#rewrite_expr addr) in
       match address with
       | XConst (IntConst n) when n#equal CHNumerical.numerical_zero ->
-         Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                ^ "Address is zero"]
+         Error [(elocm __LINE__) ^ "Address is zero"]
       | XConst (IntConst n) ->
          let dw = numerical_mod_to_doubleword n in
          if system_info#get_image_base#le dw then
            tprop
              (self#env#mk_global_variable self#l ~size n)
-             (__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
+             ((elocm __LINE__) ^ "memref:global")
          else
-           Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+           Error [(elocm __LINE__)
                   ^ "Unable to convert constant value " ^ n#toString
                   ^ "to a valid program address (should be greater than "
                   ^ system_info#get_image_base#to_hex_string
@@ -843,23 +846,23 @@ object (self)
     let address = simplify_xpr (self#inv#rewrite_expr addr) in
     let (memref_r, memoff_r) = self#decompose_memaddr address in
     TR.tbind
-      ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+      ~msg:(eloc __LINE__)
       (fun memref ->
         if memref#is_global_reference then
           TR.tbind
-            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
+            ~msg:((elocm __LINE__) ^ "memref:global")
             (fun memoff ->
               TR.tbind
-                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                ~msg:(eloc __LINE__)
                 (self#env#mk_global_variable ~size self#l)
                 (get_total_constant_offset memoff))
             memoff_r
         else
           TR.tbind
-            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+            ~msg:(eloc __LINE__)
             (fun memoff ->
               TR.tmap
-                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                ~msg:(eloc __LINE__)
                 (self#env#mk_memory_variable memref)
                 (get_total_constant_offset memoff))
             memoff_r)
@@ -911,10 +914,10 @@ object (self)
           self#get_var_at_address ~size:(Some size) address
         else
           TR.tbind
-            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+            ~msg:(eloc __LINE__)
             (fun memoff ->
               TR.tmap
-                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                ~msg:(eloc __LINE__)
                 (self#env#mk_memory_variable memref)
                 (get_total_constant_offset memoff))
             memoff_r)
@@ -1053,7 +1056,6 @@ object (self)
    * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
 
   method get_singleton_stackpointer_offset: numerical_t traceresult =
-    let ename = "get_singleton_stackpointer_offset" in
     let arch = system_settings#get_architecture in
     let roffset = self#get_stackpointer_offset arch in
     match roffset with
@@ -1061,9 +1063,9 @@ object (self)
        (match sprange#singleton with
         | Some num -> Ok num
         | _ ->
-           Error [ename ^ ": " ^ (self#stackpointer_offset_to_string arch)])
+           Error [(elocm __LINE__) ^ (self#stackpointer_offset_to_string arch)])
     | (level, _) ->
-       Error [ename ^ ": level: " ^ (string_of_int level)]
+       Error [(elocm __LINE__) ^ ": level: " ^ (string_of_int level)]
 
   method get_stackpointer_offset arch =
     match arch with
@@ -1279,19 +1281,19 @@ object (self)
     | XOp ((Xf "addressofvar"), [XVar v]) when self#env#is_global_variable v ->
        let gvaddr_r = self#f#env#get_global_variable_address v in
        TR.tbind
-         ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+         ~msg:(eloc __LINE__)
          (fun gvaddr ->
            if memmap#has_location gvaddr then
              let gloc = memmap#get_location gvaddr in
              let varresult =
                TR.tmap
-                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 ~msg:(eloc __LINE__)
                  (fun offset -> self#f#env#mk_gloc_variable gloc offset)
                  (gloc#address_offset_memory_offset
                     ~tgtsize:size ~tgtbtype:btype self#l zero_constant_expr) in
              varresult
            else
-             Error[__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+             Error[(elocm __LINE__)
                    ^ (p2s self#l#toPretty)
                    ^ ": "
                    ^ "Global location at address "
@@ -1302,15 +1304,15 @@ object (self)
     | XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); xoff])
          when self#f#env#is_global_variable v ->
        let gvaddr_r = self#f#env#get_global_variable_address v in
-       let cxoff_r = self#convert_xpr_to_c_expr xoff in
+       let cxoff_r = self#xpr_to_cxpr xoff in
        TR.tbind
-         ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+         ~msg:(eloc __LINE__)
          (fun gvaddr ->
            if memmap#has_location gvaddr then
              let gloc = memmap#get_location gvaddr in
              let varresult =
                TR.tmap
-                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 ~msg:(eloc __LINE__)
                  (fun offset -> self#f#env#mk_gloc_variable gloc offset)
                  (TR.tbind
                     (fun xoff ->
@@ -1328,7 +1330,7 @@ object (self)
              varresult
 
            else
-             Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+             Error [(elocm __LINE__)
                     ^ (p2s self#l#toPretty)
                     ^ ": "
                     ^ "Global location at address "
@@ -1339,18 +1341,70 @@ object (self)
        match memmap#xpr_containing_location addrvalue with
        | Some gloc ->
           (TR.tmap
-             ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+             ~msg:(eloc __LINE__)
              (fun offset -> self#f#env#mk_gloc_variable gloc offset)
              (gloc#address_memory_offset
                 ~tgtsize:size ~tgtbtype:btype self#l addrvalue))
        | _ ->
           let (memref_r, memoff_r) = self#decompose_memaddr addrvalue in
           TR.tmap2
-            ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+            ~msg1:(eloc __LINE__)
             (fun memref memoff ->
               self#f#env#mk_offset_memory_variable memref memoff)
             memref_r memoff_r
 
+  (* deprecated. to be merged with get_var_at_address *)
+   method get_lhs_from_address (xpr:xpr_t) =
+     let xpr = self#inv#rewrite_expr xpr in
+     let default () =
+       self#env#mk_memory_variable
+         (self#env#mk_unknown_memory_reference "lhs-from-address")
+         numerical_zero in
+     match xpr with
+     | XConst (IntConst n) when n#gt numerical_zero ->
+        log_tfold_default
+          (mk_tracelog_spec
+             ~tag:"get_lhs_from_address"
+             (self#cia ^ ": constant: " ^ n#toString))
+          (fun base ->
+            if system_info#get_image_base#le base then
+              log_tfold_default
+                (log_error
+                   "get_lhs_from_address"
+                   (self#cia ^ ": constant: " ^ n#toString))
+                (fun v -> v)
+                (default ())
+	        (self#env#mk_global_variable self#l n)
+            else
+              default ())
+          (default ())
+          (numerical_to_doubleword n)
+     | _ ->
+        default ()
+
+   (* Handles the following cases:
+      - initial_register_value:
+         if the register is a function parameter: get parameter type
+         otherwise: Error
+
+      - initial_memory_value:
+         get type of corresponding memory variable
+
+      - memory_variable:
+         separate base from offset
+         * global: retrieve type from global-memory-map if addresses match
+           otherwise: Error
+           Note: this may lead to confusion between type of first field and
+               type of struct
+
+         * basevar:
+           if no-offset: type-of *basevar
+           otherwise: type dependent on offset
+
+      - return_value:
+        if callsite has a typed var-intro: retrieve type of var-intro
+        otherwise: Error (not yet handled)
+    *)
   method get_variable_type (v: variable_t): btype_t traceresult =
     let is_zero (x: xpr_t) =
       match x with
@@ -1359,7 +1413,7 @@ object (self)
     if self#f#env#is_initial_register_value v then
       let reg_r = self#f#env#get_initial_register_value_register v in
       TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+        ~msg:(eloc __LINE__)
         (fun reg ->
           if self#f#get_summary#has_parameter_for_register reg then
             let param = self#f#get_summary#get_parameter_for_register reg in
@@ -1367,22 +1421,17 @@ object (self)
           else
             let ty = self#env#get_variable_type v in
             match ty with
-            | None ->
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                      ^ "variable: " ^ (x2s (XVar v))]
+            | None -> Error [(elocm __LINE__) ^ "variable: " ^ (x2s (XVar v))]
             | Some t -> Ok t)
         reg_r
     else if self#env#is_initial_memory_value v then
       let memvar_r = self#env#get_init_value_variable v in
-      TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-        self#get_variable_type
-        memvar_r
+      TR.tbind ~msg:(eloc __LINE__) self#get_variable_type memvar_r
     else if self#env#is_memory_variable v then
       let memref_r = self#env#get_memory_reference v in
       let memoff_r = self#env#get_memvar_offset v in
       TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+        ~msg:(eloc __LINE__)
         (fun memref ->
           match memref#get_base with
           | BGlobal ->
@@ -1393,26 +1442,25 @@ object (self)
                    let gloc = memmap#get_location gvaddr in
                    Ok (gloc#btype)
                  else
-                   Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                   Error [(elocm __LINE__)
                           ^ "no global location found for address "
                           ^ gvaddr#to_hex_string]
               | _ ->
-                 Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                        ^ "not a constant offset"])
+                 Error [(elocm __LINE__) ^ "not a constant offset"])
           | _ ->
              let basevar_r =
                match memref#get_base with
                | BaseVar v -> Ok v
                | b ->
-                  Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                  Error [(elocm __LINE__)
                          ^ "memory-base: " ^ (p2s (memory_base_to_pretty b))] in
              let basevar_type_r =
                TR.tbind
-                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 ~msg:(eloc __LINE__)
                  self#get_variable_type
                  basevar_r in
              TR.tbind
-               ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+               ~msg:(eloc __LINE__)
                (fun basevartype ->
                  TR.tbind
                    (fun memoff ->
@@ -1424,7 +1472,7 @@ object (self)
                           address_memory_offset
                             (ptr_deref basevartype) (num_constant_expr n) in
                         TR.tbind
-                          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                          ~msg:((elocm __LINE__)
                                 ^ "basevar type: " ^ (btype_to_string basevartype)
                                 ^ "; offset: " ^ n#toString)
                           (fun off ->
@@ -1434,7 +1482,7 @@ object (self)
                                let finfo = get_compinfo_field cinfo fname in
                                Ok finfo.bftype
                             | _ ->
-                               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                               Error [(elocm __LINE__)
                                       ^ "symbolic offset: "
                                       ^ (memory_offset_to_string off)
                                       ^ " with basevar type: "
@@ -1446,7 +1494,7 @@ object (self)
                         let finfo = get_compinfo_field cinfo fname in
                         Ok finfo.bftype
                      | IndexOffset (v, i, memsuboff) ->
-                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                        Error [(elocm __LINE__)
                                ^ "index offset: "
                                ^ (memory_offset_to_string memoff)
                                ^ " with "
@@ -1456,7 +1504,7 @@ object (self)
                                ^ "; and "
                                ^ (memory_offset_to_string memsuboff)]
                      | ArrayIndexOffset (x, memsuboff) ->
-                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                        Error [(elocm __LINE__)
                                ^ "array index offset: "
                                ^ (memory_offset_to_string memoff)
                                ^ " with "
@@ -1467,14 +1515,14 @@ object (self)
                         (match basevartype with
                          | TPtr (t, _) -> Ok t
                          | _ ->
-                            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                            Error [(elocm __LINE__)
                                    ^ "array index offset: "
                                    ^ (memory_offset_to_string memoff)
                                    ^ " with basevar type: "
                                    ^ (btype_to_string basevartype)
                                    ^ " not yet handled"])
                      | BasePtrArrayIndexOffset (x, memsuboff) ->
-                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                        Error [(elocm __LINE__)
                                ^ "base-ptr array index offset: "
                                ^ (memory_offset_to_string memoff)
                                ^ " with "
@@ -1483,55 +1531,121 @@ object (self)
                                ^ (memory_offset_to_string memsuboff)]
 
                      | _ ->
-                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                        Error [(elocm __LINE__)
                                ^ "memoff: " ^ (memory_offset_to_string memoff)
                                ^ " not yet handled"])
                    memoff_r)
                basevar_type_r)
       memref_r
     else if self#f#env#is_return_value v then
-      let callsite_r = self#f#env#get_call_site v in
       TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+        ~msg:(eloc __LINE__)
         (fun callsite ->
           let loc = ctxt_string_to_location self#fa callsite in
           let fndata = functions_data#get_function self#fa in
           if fndata#has_regvar_type_annotation loc#i then
             fndata#get_regvar_type_annotation loc#i
           else
-            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+            Error [(elocm __LINE__)
                    ^ "type of callsite return value " ^ (x2s (XVar v))
                    ^ " at address " ^ loc#i#to_hex_string
                    ^ " not yet handled"])
-        callsite_r
+        (self#f#env#get_call_site v)
+    else if self#f#env#is_register_variable v then
+      let vrdefs = self#get_variable_rdefs v in
+      let fndata = self#f#get_function_data in
+      match vrdefs with
+      | h :: _ ->
+         let optty_r =
+           TR.tmap
+             (fun r -> fndata#get_reglhs_type r h#getBaseName)
+             (self#f#env#get_register v) in
+         TR.tfold
+           ~ok:(fun optty ->
+             match optty with
+             | Some ty -> Ok ty
+             | _ ->
+                Error [
+                    (elocm __LINE__)
+                    ^ "No reglhs type assignment found for variable "
+                    ^ (p2s v#toPretty)
+                    ^ " at location "
+                    ^ h#getBaseName])
+           ~error:(fun e -> Error ((elocm __LINE__) :: e))
+         optty_r
+      | _ ->
+         Error [
+             (elocm __LINE__)
+             ^ "Unable to find reachingdefs for variable "
+             ^ (p2s v#toPretty)]
     else
       let ty = self#env#get_variable_type v in
       match ty with
-      | None ->
-         Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                ^ "variable: " ^ (x2s (XVar v))]
+      | None -> Error [(elocm __LINE__) ^ "variable: " ^ (x2s (XVar v))]
       | Some t -> Ok t
 
-  method convert_xpr_to_c_expr
-           ?(size=None) ?(xtype=None) (x: xpr_t): xpr_t traceresult =
+  method private get_variable_rdefs (v: variable_t): symbol_t list =
+    let symvar = self#f#env#mk_symbolic_variable v in
+    let varinvs = self#varinv#get_var_reaching_defs symvar in
+    (match varinvs with
+     | [vinv] -> vinv#get_reaching_defs
+     | _ ->
+        List.concat (List.map (fun vinv -> vinv#get_reaching_defs) varinvs))
+
+  method xpr_to_cxpr
+           ?(arithm=false)
+           ?(size=None)
+           ?(xtype=None)
+           (x: xpr_t): xpr_t traceresult =
     let _ =
       log_diagnostics_result
         ~msg:(p2s self#l#toPretty)
-        ~tag:"convert_xpr_to_c_expr"
+        ~tag:"xpr_to_cxpr"
         __FILE__ __LINE__
         ["size: " ^ (opti2s size);
          "xtype: " ^ (optty2s xtype);
          "x: " ^ (x2s x)] in
-    match xtype with
-    | None -> self#convert_xpr_offsets ~size x
-    | Some t ->
-       match x with
-       | XConst (IntConst n)
-            when n#equal (mkNumerical 0xffffffff) && is_int t ->
-          Ok (int_constant_expr (-1))
-       | _ -> self#convert_xpr_offsets ~xtype ~size x
-
-  method convert_addr_to_c_pointed_to_expr
+    let is_pointer (y: xpr_t) =
+      TR.tfold_default BCHBCTypeUtil.is_pointer false (self#get_xpr_type y) in
+    let default () = self#convert_xpr_offsets ~xtype ~size x in
+    match x with
+    | XOp (XPlus, [y; XConst (IntConst n)]) when is_pointer y && arithm ->
+       let derefty = BCHBCTypeUtil.ptr_deref (TR.tget_ok (self#get_xpr_type y)) in
+       let _ =
+         log_diagnostics_result
+           ~msg:(p2s self#l#toPretty)
+           ~tag:"xpr_to_cxpr:pointer expression"
+           __FILE__ __LINE__
+           ["x: " ^ (x2s x); "*ty: " ^ (ty2s derefty)] in
+       TR.tmap2
+         ~msg1:(eloc __LINE__)
+         ~msg2:(eloc __LINE__)
+         (fun cy size ->
+           let scaledincr = XConst (IntConst (n#div (mkNumerical size))) in
+           let result = XOp (XPlus, [cy; scaledincr]) in
+           let _ =
+             log_diagnostics_result
+               ~msg:(p2s self#l#toPretty)
+               ~tag:"xpr_to_cxpr:pointer expression"
+               __FILE__ __LINE__
+               ["x: " ^ (x2s x);
+                "cy: " ^ (x2s cy);
+                "size: " ^ (i2s size);
+                "result: " ^ (x2s result)] in
+           result)
+         (self#xpr_to_cxpr y)
+         (BCHBCTypeUtil.size_of_btype derefty)
+    | _ ->
+       match xtype with
+       | None -> default ()
+       | Some t ->
+          match x with
+          | XConst (IntConst n)
+               when n#equal (mkNumerical 0xffffffff) && is_int t ->
+             Ok (int_constant_expr (-1))
+          | _ -> default ()
+
+  method addr_to_ctgt_xpr
            ?(size=None) ?(xtype=None) (a: xpr_t): xpr_t traceresult =
     let vars = vars_as_positive_terms a in
     let knownpointers =
@@ -1541,7 +1655,7 @@ object (self)
         ) vars in
     let _ =
       log_diagnostics_result
-        ~tag:"convert_addr_to_c_pointed_to_expr"
+        ~tag:"addr_to_ctgt_xpr"
         __FILE__ __LINE__
         [(p2s self#l#toPretty);
          "known pointers: ";
@@ -1557,13 +1671,13 @@ object (self)
          | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
          | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
          | _ ->
-            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+            Error [(elocm __LINE__)
                    ^ "base: " ^ (p2s base#toPretty)
                    ^ "; offset expr: " ^ (x2s offset)] in
        let var_r =
          TR.tmap2
-           ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-           ~msg2:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           ~msg1:(eloc __LINE__)
+           ~msg2:(eloc __LINE__)
            (fun memref memoff ->
              self#env#mk_offset_memory_variable memref memoff)
            memref_r memoff_r in
@@ -1573,118 +1687,49 @@ object (self)
        let offset = simplify_xpr (XOp (XMinus, [a; XVar base])) in
        let memref_r = self#env#mk_base_variable_reference base in
        let vartype_r = self#get_variable_type base in
-       let rvartype_r =
-         TR.tbind
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-           resolve_type
-           vartype_r in
+       let rvartype_r = TR.tbind ~msg:(eloc __LINE__) resolve_type vartype_r in
        let basetype_r =
          TR.tbind
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           ~msg:(eloc __LINE__)
            (fun t ->
              if is_pointer t then
                Ok (ptr_deref t)
              else
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ "x: " ^ (x2s a) ^ "; base: " ^ (x2s (XVar base))
                       ^ "; offset: " ^ (x2s offset)])
            rvartype_r in
        let memoff_r =
          TR.tbind
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                 ^ "base pointer: " ^ (x2s (XVar base)))
+           ~msg:((elocm __LINE__) ^ "base pointer: " ^ (x2s (XVar base)))
            (fun basetype -> address_memory_offset basetype offset)
            basetype_r in
        let var_r =
          TR.tmap2
-           ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-           ~msg2:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           ~msg1:(eloc __LINE__)
+           ~msg2:(eloc __LINE__)
            (fun memref memoff ->
              self#env#mk_offset_memory_variable memref memoff)
            memref_r memoff_r in
        TR.tmap (fun v -> XVar v) var_r
     | _ ->
-       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+       Error [(elocm __LINE__)
               ^ "size: " ^ (opti2s size) ^ "; "
               ^ "type: " ^ (optty2s xtype) ^ "; "
               ^ "addr: " ^ (x2s a)
               ^ ": Not yet handled"]
 
-  method convert_var_to_c_variable
+  method var_to_cvar
            ?(size=None) ?(vtype=None) (v: variable_t): variable_t traceresult =
     match vtype with
     | None -> self#convert_variable_offsets ~size v
     | _ ->
-       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+       Error [(elocm __LINE__)
               ^ "size: " ^ (opti2s size) ^ "; "
               ^ "type: " ^ (optty2s vtype) ^ "; "
               ^ "v: " ^ (p2s v#toPretty)
               ^ ": Not yet implemented"]
 
-  method convert_addr_to_c_pointed_to_variable
-           ?(size=None) ?(vtype=None) (a: xpr_t): variable_t traceresult =
-    let vars = vars_as_positive_terms a in
-    let knownpointers = List.filter self#f#is_base_pointer vars in
-    match knownpointers with
-    (* one known pointer, must be the base *)
-    | [base] when self#f#env#is_initial_stackpointer_value base ->
-       let offset = simplify_xpr (XOp (XMinus, [a; XVar base])) in
-       let memref_r = self#env#mk_base_variable_reference base in
-       let memoff_r =
-         match offset with
-         | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
-         | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
-         | _ ->
-            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                   ^ "base: " ^ (p2s base#toPretty)
-                   ^ "; offset expr: " ^ (x2s offset)] in
-       TR.tmap2
-         ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-         ~msg2:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-         (fun memref memoff ->
-           self#env#mk_offset_memory_variable memref memoff)
-         memref_r memoff_r
-
-    | [base] ->
-       let offset = simplify_xpr (XOp (XMinus, [a; XVar base])) in
-       let memref_r = self#env#mk_base_variable_reference base in
-       let vartype_r = self#get_variable_type base in
-       let rvartype_r =
-         TR.tbind
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-           resolve_type
-           vartype_r in
-       let basetype_r =
-         TR.tbind
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-           (fun t ->
-             if is_pointer t then
-               Ok (ptr_deref t)
-             else
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                      ^ "x: " ^ (x2s a) ^ "; base: " ^ (x2s (XVar base))
-                      ^ "; offset: " ^ (x2s offset)])
-           rvartype_r in
-       let memoff_r =
-         TR.tbind
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                 ^ "base pointer: " ^ (x2s (XVar base)))
-           (fun basetype -> address_memory_offset basetype offset)
-           basetype_r in
-       TR.tmap2
-         ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-         ~msg2:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-         (fun memref memoff ->
-           self#env#mk_offset_memory_variable memref memoff)
-         memref_r memoff_r
-    | _ ->
-       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ "size: " ^ (opti2s size) ^ "; "
-              ^ "vtype: " ^ (optty2s vtype) ^ "; "
-              ^ "addr: " ^ (x2s a)
-              ^ ": Not yet handled"]
-
-
   method convert_variable_offsets
            ?(vtype=None) ?(size=None) (v: variable_t): variable_t traceresult =
     let _ =
@@ -1703,27 +1748,28 @@ object (self)
       let optvtype = match vtype with Some t -> t | _ -> t_unknown in
       let tgttype_r =
         TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+          ~msg:(eloc __LINE__)
           (fun basetype ->
             match basetype with
             | TPtr (t, _) -> Ok t
             | t ->
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ "Type " ^ (btype_to_string t)
                       ^ " is not a pointer"]) basetype_r in
       let coffset_r =
         TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+          ~msg:(eloc __LINE__)
           (fun offset ->
             match offset with
             | ConstantOffset (n, NoOffset) ->
                TR.tbind
-                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 ~msg:(eloc __LINE__)
                  (fun tgttype ->
                    address_memory_offset
                      ~tgtbtype:optvtype ~tgtsize:size tgttype (num_constant_expr n))
                  tgttype_r
-            | _ -> Ok offset) offset_r in
+            | _ ->
+               Ok offset) offset_r in
       let _ =
         log_diagnostics_result
           ~msg:(p2s self#l#toPretty)
@@ -1734,7 +1780,7 @@ object (self)
            "offset : " ^ (TR.tfold_default memory_offset_to_string "?" offset_r);
            "coffset: " ^ (TR.tfold_default memory_offset_to_string "?" coffset_r)] in
       TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))
+        ~msg:((elocm __LINE__) ^ (p2s v#toPretty))
         (fun cbasevar ->
           TR.tbind
             (fun coffset ->
@@ -1769,22 +1815,22 @@ object (self)
       let basetype_r = TR.tbind self#get_variable_type cbasevar_r in
       let tgttype_r =
         TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+          ~msg:(eloc __LINE__)
           (fun basetype ->
             match basetype with
             | TPtr (t, _) -> Ok t
             | TComp (key, _) ->
                let cinfo = get_compinfo_by_key key in
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ "Target type is a struct: " ^ cinfo.bcname
                       ^ ". A pointer was expected"]
             | t ->
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ "Type " ^ (btype_to_string t)
                       ^ " is not a pointer"]) basetype_r in
       let coffset_r =
         TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+          ~msg:(eloc __LINE__)
           (fun offset ->
             match offset with
             | NoOffset ->
@@ -1795,28 +1841,28 @@ object (self)
                    __FILE__ __LINE__
                    ["v: " ^ (p2s v#toPretty)] in
                TR.tbind
-                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 ~msg:(eloc __LINE__)
                  (fun tgttype ->
                    address_memory_offset
                      ~tgtsize:size tgttype (int_constant_expr 0)) tgttype_r
             | ConstantOffset (n, NoOffset) ->
                TR.tbind
-                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 ~msg:(eloc __LINE__)
                  (fun tgttype ->
                    address_memory_offset
                      ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r
-            | _ -> Ok offset) offset_r in
+            | _ ->
+               Ok offset) offset_r in
       TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))
+        ~msg:((elocm __LINE__) ^ (p2s v#toPretty))
         (fun cbasevar ->
           TR.tbind
-            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                  ^ "cbasevar: " ^ (p2s cbasevar#toPretty))
+            ~msg:((elocm __LINE__) ^ "cbasevar: " ^ (p2s cbasevar#toPretty))
             (fun coffset ->
               let memvar_r =
                 self#env#mk_basevar_memory_variable cbasevar coffset in
               TR.tbind
-                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                ~msg:((elocm __LINE__)
                       ^ "cbasevar: " ^ (p2s cbasevar#toPretty)
                       ^ "; coffset: " ^ (memory_offset_to_string coffset))
                 self#env#mk_initial_memory_value memvar_r
@@ -1843,12 +1889,11 @@ object (self)
       match exp with
       | XVar v when self#env#is_basevar_memory_value v ->
          TR.tmap
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                 ^ (p2s v#toPretty))
+           ~msg:((elocm __LINE__) ^ (p2s v#toPretty))
            (fun v -> XVar v) (self#convert_value_offsets ~size v)
       | XVar v when self#env#is_basevar_memory_variable v ->
          TR.tmap
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           ~msg:(eloc __LINE__)
            (fun v -> XVar v) (self#convert_variable_offsets ~size v)
       | XOp ((Xf "addressofvar"), [XVar v]) ->
          let derefty =
@@ -1858,7 +1903,7 @@ object (self)
            | _ -> None in
          let newx_r =
            TR.tmap
-             ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+             ~msg:(eloc __LINE__)
              (fun v ->
                XVar v) (self#convert_variable_offsets ~vtype:derefty ~size v) in
          TR.tmap
@@ -1900,9 +1945,8 @@ object (self)
   method get_xpr_type (x: xpr_t): btype_t traceresult =
     match x with
     | XVar v -> self#get_variable_type v
-    | _ ->
-       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ "xpr: " ^ (x2s x)]
+    | XOp (XPlus, [XVar v; XConst (IntConst _)]) -> self#get_variable_type v
+    | _ -> Error [(elocm __LINE__) ^ "xpr: " ^ (x2s x)]
 
   method decompose_memaddr (x: xpr_t):
            (memory_reference_int traceresult * memory_offset_t traceresult) =
@@ -1926,7 +1970,7 @@ object (self)
          | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
          | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
          | _ ->
-            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+            Error [(elocm __LINE__)
                    ^ "base: " ^ (p2s base#toPretty)
                    ^ "; offset expr: " ^ (x2s offset)] in
        (memref_r, memoff_r)
@@ -1952,7 +1996,7 @@ object (self)
               let v = self#env#mk_symbolic_value x in
               Ok (IndexOffset (v, n#toInt, NoOffset))
            | _ ->
-              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+              Error [(elocm __LINE__)
                      ^ (p2s self#l#toPretty) ^ ": "
                      ^ "decompose_memaddr: " ^ (x2s x) ^ ": "
                      ^ "Offset from global base "
@@ -1979,7 +2023,7 @@ object (self)
                | XOp (XMult, [XConst (IntConst n); XVar v]) ->
                   Ok (IndexOffset (v, n#toInt, NoOffset))
               | _ ->
-                 Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                 Error [(elocm __LINE__)
                         ^ (p2s self#l#toPretty) ^ ": "
                         ^ "decompose_memaddr: " ^ (x2s x) ^ ": "
                         ^ "Offset from base "
@@ -2010,7 +2054,7 @@ object (self)
                    | XOp (XMult, [XConst (IntConst n); XVar v]) ->
                       Ok (IndexOffset (v, n#toInt, NoOffset))
                    | _ ->
-                      Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                      Error [(elocm __LINE__)
                              ^ (p2s self#l#toPretty) ^ ": "
                              ^ "decompose_memaddr: " ^ (x2s x) ^ ": "
                              ^ "Offset from base "
@@ -2021,49 +2065,45 @@ object (self)
 
           | [v] ->
              let memref_r =
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ (p2s self#l#toPretty) ^ ": "
                       ^ "No candidate base pointers. Only variable found: "
                       ^ (p2s v#toPretty)] in
-             let memoff_r =
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
+             let memoff_r = Error [eloc __LINE__] in
              (memref_r, memoff_r)
 
           | [] ->
              let memref_r =
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ (p2s self#l#toPretty) ^ ": "
                       ^ "decompose_memaddr: " ^ (x2s x) ^ ": "
                       ^ "No candidate pointers. Left with maxC: "
                       ^ maxC#toString] in
-             let memoff_r =
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
+             let memoff_r = Error [(eloc __LINE__)] in
              (memref_r, memoff_r)
 
           (* multiple variables *)
           | _ ->
              let memref_r =
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               Error [(elocm __LINE__)
                       ^ (p2s self#l#toPretty) ^ ": "
                       ^ "decompose_memaddr: " ^ (x2s x) ^ ": "
                       ^ "Multiple variables: "
                       ^ (String.concat "; "
                            (List.map (fun v -> p2s v#toPretty) vars))] in
-             let memoff_r =
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
+             let memoff_r = Error [(eloc __LINE__)] in
              (memref_r, memoff_r))
 
     (* multiple known pointers *)
     | _ ->
        let memref_r =
-         Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+         Error [(elocm __LINE__)
                 ^ (p2s self#l#toPretty) ^ ": "
                 ^ "decompose_memaddr: " ^ (x2s x) ^ ": "
                 ^ "Multiple known pointers: "
                 ^ (String.concat "; "
                      (List.map (fun v -> p2s v#toPretty) knownpointers))] in
-       let memoff_r =
-         Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
+       let memoff_r = Error [(eloc __LINE__)] in
        (memref_r, memoff_r)
 
   (* the objective is to extract a base pointer and an offset expression
@@ -2220,34 +2260,6 @@ object (self)
 	 default ()
        end
 
-   method get_lhs_from_address (xpr:xpr_t) =
-     let xpr = self#inv#rewrite_expr xpr in
-     let default () =
-       self#env#mk_memory_variable
-         (self#env#mk_unknown_memory_reference "lhs-from-address")
-         numerical_zero in
-     match xpr with
-     | XConst (IntConst n) when n#gt numerical_zero ->
-        log_tfold_default
-          (mk_tracelog_spec
-             ~tag:"get_lhs_from_address"
-             (self#cia ^ ": constant: " ^ n#toString))
-          (fun base ->
-            if system_info#get_image_base#le base then
-              log_tfold_default
-                (log_error
-                   "get_lhs_from_address"
-                   (self#cia ^ ": constant: " ^ n#toString))
-                (fun v -> v)
-                (default ())
-	        (self#env#mk_global_variable self#l n)
-            else
-              default ())
-          (default ())
-          (numerical_to_doubleword n)
-     | _ ->
-        default ()
-
    method get_bridge_variable_value (par_index:int) (var:variable_t) =
      if self#f#has_constant var then
        num_constant_expr (self#f#get_constant var )
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml
index 009125c0..84ef74e0 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml
@@ -134,6 +134,8 @@ object (self)
   val mutable functiontype = t_unknown
   val mutable callsites = 0
   val mutable pathcontexts = []  (* (ctxt_iaddress_t, ctxt_iaddress_t list) list *)
+  val mutable reglhstypes = []  (* (register_t * iaddr * btype_t option) list *)
+  val mutable stacklhstypes = [] (* (offset * btype_t option) list *)
 
   method set_function_type (ty: btype_t) = functiontype <- ty
 
@@ -174,6 +176,30 @@ object (self)
 
   method has_callsites = callsites > 0
 
+  method set_reglhs_types (regtypes: (register_t * string * btype_t option) list) =
+    reglhstypes <- regtypes
+
+  method get_reglhs_types = reglhstypes
+
+  method get_reglhs_type (reg: register_t) (iaddr: string): btype_t option =
+    List.fold_left (fun acc (r, i, t) ->
+        match acc with
+        | Some _ -> acc
+        | _ ->
+           if BCHCPURegisters.register_equal reg r && i = iaddr then t else acc)
+      None reglhstypes
+
+  method set_stack_offset_types (stacktypes: (int * btype_t option) list) =
+    stacklhstypes <- stacktypes
+
+  method get_stack_offset_types = stacklhstypes
+
+  method get_stack_offset_type (offset: int): btype_t option =
+    List.fold_left (fun acc (o, t) ->
+        match acc with
+        | Some _ -> acc
+        | _ -> if offset == o then t else acc) None stacklhstypes
+
   method add_name (s:string) =
     let s = sanitize_function_name s in
     if List.mem s names then
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index 0e081ad0..a6034fb8 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -1564,6 +1564,10 @@ class type function_data_int =
         returns the number of remaining call sites.*)
     method remove_callsite: int
 
+    method set_reglhs_types: ((register_t * string * btype_t option) list) -> unit
+
+    method set_stack_offset_types: ((int * btype_t option) list) -> unit
+
     (* accessors *)
     method get_names: string list  (* raw names *)
     method get_function_name: string  (* demangled or combination of all names *)
@@ -1575,6 +1579,10 @@ class type function_data_int =
     method get_inlined_blocks: doubleword_int list
     method get_function_type: btype_t
     method get_path_contexts: (string * string list) list
+    method get_reglhs_types: (register_t * string * btype_t option) list
+    method get_reglhs_type: register_t -> string -> btype_t option
+    method get_stack_offset_types: (int * btype_t option) list
+    method get_stack_offset_type: int -> btype_t option
 
     (* predicates *)
     method has_function_type: bool
@@ -6103,39 +6111,6 @@ class type floc_int =
      *)
     method decompose_address: xpr_t -> (memory_reference_int * memory_offset_t)
 
-    method convert_xpr_to_c_expr:
-             ?size:int option -> ?xtype:btype_t option -> xpr_t -> xpr_t traceresult
-
-    method convert_addr_to_c_pointed_to_expr:
-             ?size:int option -> ?xtype:btype_t option -> xpr_t -> xpr_t traceresult
-
-    method convert_var_to_c_variable:
-             ?size:int option
-             -> ?vtype:btype_t option
-             -> variable_t
-             -> variable_t traceresult
-
-    method convert_addr_to_c_pointed_to_variable:
-             ?size:int option
-             -> ?vtype:btype_t option
-             -> xpr_t
-             -> variable_t traceresult
-
-    method convert_value_offsets:
-             ?size:int option -> variable_t -> variable_t traceresult
-
-    method convert_variable_offsets:
-             ?vtype:btype_t option
-             -> ?size:int option
-             -> variable_t
-             -> variable_t traceresult
-
-    method convert_xpr_offsets:
-             ?xtype:btype_t option -> ?size:int option -> xpr_t -> xpr_t traceresult
-
-    (* returns the variable associated with the address expression *)
-    method get_lhs_from_address: xpr_t -> variable_t
-
     (* returns the value of the bridge variable for a given stack
        parameter at this instruction *)
     method get_bridge_variable_value: int -> variable_t -> xpr_t
@@ -6153,10 +6128,17 @@ class type floc_int =
              -> xpr_t               (** address value *)
              -> variable_t traceresult
 
+    (* returns the variable associated with the address expression
+       Deprecated. To be merged with get_var_at_address
+     *)
+    method get_lhs_from_address: xpr_t -> variable_t
+
     method get_variable_type: variable_t -> btype_t traceresult
 
     method get_xpr_type: xpr_t -> btype_t traceresult
 
+
+
     (** {2 Predicates on variables}*)
 
     (* returns true if the given variable evaluates to a constant at this
@@ -6177,6 +6159,37 @@ class type floc_int =
     method has_initial_value: variable_t -> bool
 
 
+    (** {1 Conversion to c expressions / variables}*)
+
+    method xpr_to_cxpr:
+             ?arithm:bool
+             -> ?size:int option
+             -> ?xtype:btype_t option
+             -> xpr_t
+             -> xpr_t traceresult
+
+    method addr_to_ctgt_xpr:
+             ?size:int option -> ?xtype:btype_t option -> xpr_t -> xpr_t traceresult
+
+    method var_to_cvar:
+             ?size:int option
+             -> ?vtype:btype_t option
+             -> variable_t
+             -> variable_t traceresult
+
+    method convert_value_offsets:
+             ?size:int option -> variable_t -> variable_t traceresult
+
+    method convert_variable_offsets:
+             ?vtype:btype_t option
+             -> ?size:int option
+             -> variable_t
+             -> variable_t traceresult
+
+    method convert_xpr_offsets:
+             ?xtype:btype_t option -> ?size:int option -> xpr_t -> xpr_t traceresult
+
+
     (** {1 Conditional jumps}*)
 
     (* sets the test expression for this instruction *)
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 270b8754..90d81fca 100644
--- a/CodeHawk/CHB/bchlib/bCHVersion.ml
+++ b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250822"
-  ~date:"2025-08-22"
+  ~version:"0.6.0_20250830"
+  ~date:"2025-08-30"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
index cb8504f8..a9ae102f 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
@@ -284,7 +284,7 @@ object (self)
   val typeconstraintstore = mk_type_constraint_store ()
 
   method record_results ?(save=true) (fn:arm_assembly_function_int) =
-    let fndata = new fn_analysis_results_t fn in
+    let fnadata = new fn_analysis_results_t fn in
     let vard = (get_function_info fn#get_address)#env#varmgr#vard in
     let typeconstraints =
       mk_arm_fn_type_constraints typeconstraintstore fn in
@@ -292,18 +292,20 @@ object (self)
     begin
       (if save then
          let faddr = fn#get_address#to_hex_string in
+         let fndata = BCHFunctionData.functions_data#get_function fn#get_address in
          begin
-           fndata#write_xml node;
            typeconstraints#record_type_constraints;
-           fndata#write_xml_register_types node
-             (typeconstraintstore#resolve_reglhs_types faddr);
-           fndata#write_xml_stack_types node
+           fndata#set_reglhs_types (typeconstraintstore#resolve_reglhs_types faddr);
+           fndata#set_stack_offset_types
              (typeconstraintstore#resolve_local_stack_lhs_types faddr);
+           fnadata#write_xml_register_types node fndata#get_reglhs_types;
+           fnadata#write_xml_stack_types node fndata#get_stack_offset_types;
+           fnadata#write_xml node;
            node#setAttribute "a" faddr;
            save_app_function_results_file faddr node;
            save_vars faddr vard
          end );
-           (* (if save then fndata#save); *)
+           (* (if save then fnadata#save); *)
       H.add table fn#get_address#to_hex_string fn
     end
 
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
index 07d1951b..234a000f 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
@@ -380,7 +380,7 @@ object (self)
       let cbutag = "cbu:" ^ (string_of_int (argslen + 4)) in
       let tags = xtag :: ((List.tl tags) @ [vbutag; xbutag; cbutag]) in
       let xx = TR.tmap rewrite_expr x in
-      let cx = TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xx in
+      let cx = TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xx in
       let args =
         args
         @ [index_variable v;
@@ -557,8 +557,8 @@ object (self)
             should have been made position independent for local variables.*)
          let tcond = rewrite_expr txpr in
          let fcond = rewrite_expr fxpr in
-         let ctcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) tcond in
-         let cfcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) fcond in
+         let ctcond_r = floc#xpr_to_cxpr ~size:(Some 4) tcond in
+         let cfcond_r = floc#xpr_to_cxpr ~size:(Some 4) fcond in
          let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in
          let argslen = List.length args in
          let xtag = "xxcc" ^ (string_repeat "r" (List.length rdefs)) in
@@ -699,7 +699,7 @@ object (self)
                         (floc#get_var_at_address ~btype:(ptr_deref ptype) xx)
               else
                 xx in
-            let cx_r = floc#convert_xpr_to_c_expr ~xtype:(Some ptype) xx in
+            let cx_r = floc#xpr_to_cxpr ~xtype:(Some ptype) xx in
             let rdef = get_rdef_r xvar_r in
             (xx :: xprs,
              cx_r :: cxprs_r,
@@ -796,7 +796,7 @@ object (self)
          let xxrm_r = TR.tmap rewrite_expr xrm_r in
          let rresult_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~arithm:true ~size:(Some 4)) rresult_r in
          let _ =
            TR.tfold_default
              (fun r -> ignore (get_string_reference floc r)) () rresult_r in
@@ -829,7 +829,7 @@ object (self)
          let xxrm_r = TR.tmap rewrite_expr xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let _ =
            TR.tfold_default
              (fun r -> ignore (get_string_reference floc r)) () rresult_r in
@@ -849,7 +849,7 @@ object (self)
          let vrd_r = rd#to_variable floc in
          let ximm_r = imm#to_expr floc in
          let caddr_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) ximm_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) ximm_r in
          let _ =
            TR.tfold_default
              (fun x -> ignore (get_string_reference floc x)) () ximm_r in
@@ -878,7 +878,7 @@ object (self)
              xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -935,7 +935,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XBAnd, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -958,7 +958,7 @@ object (self)
              xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -980,7 +980,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XBXor, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -1007,7 +1007,7 @@ object (self)
          let result_r = TR.tmap (fun xrm -> XOp (XBNot, [xrm])) xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs = [get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
          let useshigh = [get_def_use_high_r vrd_r] in
@@ -1027,7 +1027,7 @@ object (self)
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XBOr, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
-         let cresult_r = TR.tbind floc#convert_xpr_to_c_expr rresult_r in
+         let cresult_r = TR.tbind floc#xpr_to_cxpr rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -1113,7 +1113,7 @@ object (self)
            let xrn_r = indexregop#to_expr floc in
            let xxrn_r = TR.tmap rewrite_expr xrn_r in
            let cxrn_r =
-             TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxrn_r in
+             TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xxrn_r in
            let rdefs = (get_rdef_r xrn_r) :: (get_all_rdefs_r xxrn_r) in
            let (tagstring, args) =
              mk_instrx_data_r
@@ -1142,8 +1142,8 @@ object (self)
             should have been made position independent for local variables.*)
          let tcond = rewrite_expr txpr in
          let fcond = rewrite_expr fxpr in
-         let ctcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) tcond in
-         let cfcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) fcond in
+         let ctcond_r = floc#xpr_to_cxpr ~size:(Some 4) tcond in
+         let cfcond_r = floc#xpr_to_cxpr ~size:(Some 4) fcond in
          let csetter_addr_r = string_to_doubleword csetter in
          let csetter_instr_r =
            TR.tbind get_arm_assembly_instruction csetter_addr_r in
@@ -1189,7 +1189,7 @@ object (self)
          let xr0_r = r0_op#to_expr floc in
          let xxr0_r = TR.tmap rewrite_expr xr0_r in
          let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in
-         let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr xxr0_r in
+         let cxr0_r = TR.tbind floc#xpr_to_cxpr xxr0_r in
          let (tagstring, args) = mk_instrx_data_r () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let (tags, args) = add_return_value tags args xr0_r xxr0_r cxr0_r in
@@ -1267,7 +1267,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrn; xrm])) xrn_r xrm_r in
          let result_r = TR.tmap rewrite_expr xresult_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) result_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) result_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r result_r) in
          let xprs_r = [xrn_r; xrm_r; xresult_r; result_r] in
@@ -1503,7 +1503,7 @@ object (self)
                let memrhs_r = memop#to_expr floc in
                let rmemrhs_r = TR.tmap rewrite_expr memrhs_r in
                let cmemrhs_r =
-                 TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rmemrhs_r in
+                 TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rmemrhs_r in
                (mems @ [memrhs_r],
                 rmems @ [rmemrhs_r],
                 cmems @ [cmemrhs_r],
@@ -1520,7 +1520,7 @@ object (self)
                TR.tmap rewrite_expr xaddr_r) in
          let cxaddrs_r =
            List.map (fun xaddr_r ->
-               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xaddr_r)
+               TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xaddr_r)
              xaddrs_r in
          let rdefs = List.map get_rdef_r (baserhs_r :: memrhss_r) in
          let uses = List.map get_def_use_high_r (baselhs_r :: lhsvars_rl) in
@@ -1558,7 +1558,7 @@ object (self)
                let memrhs_r = memop#to_expr floc in
                let rmemrhs_r = TR.tmap rewrite_expr memrhs_r in
                let cmemrhs_r =
-                 TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rmemrhs_r in
+                 TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rmemrhs_r in
                (mems @ [memrhs_r],
                 rmems @ [rmemrhs_r],
                 cmems @ [cmemrhs_r],
@@ -1575,7 +1575,7 @@ object (self)
                TR.tmap rewrite_expr xaddr_r) in
          let cxaddrs_r =
            List.map (fun xaddr_r ->
-               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xaddr_r)
+               TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xaddr_r)
              xaddrs_r in
          let rdefs = List.map get_rdef_r (baserhs_r :: memrhss_r) in
          let uses = List.map get_def_use_high_r (baselhs_r :: lhsvars_rl) in
@@ -1665,9 +1665,9 @@ object (self)
          let uses = [get_def_use_r vrt_r] in
          let useshigh = [get_def_use_high_r vrt_r] in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrmem_r = TR.tmap rewrite_expr xmem_r in
-         let cxrmem_r = TR.tbind floc#convert_xpr_to_c_expr xrmem_r in
+         let cxrmem_r = TR.tbind floc#xpr_to_cxpr xrmem_r in
          let cxrmem_r =
            if Result.is_ok cxrmem_r then
              cxrmem_r
@@ -1678,7 +1678,7 @@ object (self)
                  ~tag:"LDR:fall-back address conversion"
                  __FILE__ __LINE__
                  ["xxaddr: " ^ (x_r2s xxaddr_r)] in
-             TR.tbind floc#convert_addr_to_c_pointed_to_expr xxaddr_r in
+             TR.tbind floc#addr_to_ctgt_xpr xxaddr_r in
          let _ =
            TR.tfold_default
              (fun xrmem -> ignore (get_string_reference floc xrmem)) () xrmem_r in
@@ -1729,10 +1729,10 @@ object (self)
          let uses = [get_def_use_r vrt_r] in
          let useshigh = [get_def_use_high_r vrt_r] in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrmem_r = TR.tmap rewrite_expr xmem_r in
          let cxrmem_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 1)) xrmem_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 1)) xrmem_r in
          let cxrmem_r =
            if Result.is_ok cxrmem_r then
              cxrmem_r
@@ -1744,7 +1744,7 @@ object (self)
                  __FILE__ __LINE__
                  ["xxaddr: " ^ (x_r2s xxaddr_r)] in
              TR.tbind
-               (floc#convert_addr_to_c_pointed_to_expr ~size:(Some 1)) xxaddr_r in
+               (floc#addr_to_ctgt_xpr ~size:(Some 1)) xxaddr_r in
          let _ =
            floc#memrecorder#record_load_r
              ~signed:false
@@ -1857,9 +1857,9 @@ object (self)
          let uses = [get_def_use_r vrt_r] in
          let useshigh = [get_def_use_high_r vrt_r] in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrmem_r = TR.tmap rewrite_expr xmem_r in
-         let cxrmem_r = TR.tbind floc#convert_xpr_to_c_expr xrmem_r in
+         let cxrmem_r = TR.tbind floc#xpr_to_cxpr xrmem_r in
          let cxrmem_r =
            if Result.is_ok cxrmem_r then
              cxrmem_r
@@ -1870,7 +1870,7 @@ object (self)
                  ~tag:"LDREX:fall-back address conversion"
                  __FILE__ __LINE__
                  ["xxaddr: " ^ (x_r2s xxaddr_r)] in
-             TR.tbind floc#convert_addr_to_c_pointed_to_expr xxaddr_r in
+             TR.tbind floc#addr_to_ctgt_xpr xxaddr_r in
          let _ =
            TR.tfold_default
              (fun xrmem -> ignore (get_string_reference floc xrmem)) () xrmem_r in
@@ -1920,15 +1920,15 @@ object (self)
          let uses = [get_def_use_r vrt_r] in
          let useshigh = [get_def_use_high_r vrt_r] in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrmem_r = TR.tmap rewrite_expr xmem_r in
          let cxrmem_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 2)) xrmem_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 2)) xrmem_r in
          let cxrmem_r =
            if Result.is_ok cxrmem_r then
              cxrmem_r
            else
-             TR.tbind floc#convert_addr_to_c_pointed_to_expr xxaddr_r in
+             TR.tbind floc#addr_to_ctgt_xpr xxaddr_r in
          let _ =
            floc#memrecorder#record_load_r
              ~signed:false
@@ -2066,7 +2066,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XLsl, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -2092,7 +2092,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XLsr, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -2135,7 +2135,7 @@ object (self)
                            let p = if inverse then XOp (XLNot, [p]) else p in
                            let rdefs = get_all_rdefs p in
                            let xp = rewrite_expr p in
-                           let cxp_r = floc#convert_xpr_to_c_expr ~size:(Some 4) xp in
+                           let cxp_r = floc#xpr_to_cxpr ~size:(Some 4) xp in
                            let (tagstring, args) =
                              mk_instrx_data_r
                                ~vars_r:[lhs_r]
@@ -2156,7 +2156,7 @@ object (self)
                        (match optpredicate with
                         | Some p ->
                            let xp = rewrite_expr p in
-                           let cxp_r = floc#convert_xpr_to_c_expr ~size:(Some 4) xp in
+                           let cxp_r = floc#xpr_to_cxpr ~size:(Some 4) xp in
                            let rdefs = get_all_rdefs p in
                            let (tagstring, args) =
                              mk_instrx_data_r
@@ -2223,7 +2223,7 @@ object (self)
          let result_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) xrm_r in
          let result_r = TR.tmap (rewrite_in_cc_context floc c) result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) result_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) result_r in
          let rdefs = (get_rdef_r xrm_r) :: (get_all_rdefs_r result_r) in
          let uses = [get_def_use_r vrd_r] in
          let useshigh = [get_def_use_high_r vrd_r] in
@@ -2297,7 +2297,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XMult, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -2412,7 +2412,7 @@ object (self)
              let xr0_r = r0_op#to_expr floc in
              let xxr0_r = TR.tmap rewrite_expr xr0_r in
              let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in
-             let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr xxr0_r in
+             let cxr0_r = TR.tbind floc#xpr_to_cxpr xxr0_r in
              add_return_value tags args xr0_r xxr0_r cxr0_r
            else
              (tags, args) in
@@ -2480,7 +2480,7 @@ object (self)
          let xxrm_r = TR.tmap rewrite_expr xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -2768,7 +2768,7 @@ object (self)
          let rrhss_rl = List.map (TR.tmap rewrite_expr) rhss_rl in
          let crhss_rl =
            List.map (fun rrhs_r ->
-               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rrhs_r)
+               TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rrhs_r)
            rrhss_rl in
          let (memlhss_rl, cmemlhss_rl, _) =
            List.fold_left
@@ -2776,8 +2776,7 @@ object (self)
                let memop = arm_reg_deref ~with_offset:off basereg WR in
                let memlhs_r = memop#to_variable floc in
                let cmemlhs_r =
-                 TR.tbind
-                   (floc#convert_var_to_c_variable ~size:(Some 4)) memlhs_r in
+                 TR.tbind (floc#var_to_cvar ~size:(Some 4)) memlhs_r in
                (lhss @ [memlhs_r],
                 clhss @ [cmemlhs_r],
                 off + 4)) ([], [], - (4 * regcount)) rl#get_register_op_list in
@@ -2794,7 +2793,7 @@ object (self)
                TR.tmap rewrite_expr xaddr_r) in
          let cxaddrs_r =
            List.map (fun xaddr_r ->
-               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xaddr_r)
+               TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xaddr_r)
            xaddrs_r in
          let rdefs = List.map get_rdef_r (baserhs_r :: rrhss_rl) in
          let uses = List.map get_def_use_r (baselhs_r :: memlhss_rl) in
@@ -2843,9 +2842,9 @@ object (self)
                    (floc#get_var_at_address ~btype:t_int x))
                xxdst_r in
            let csrc_r =
-             TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxsrc_r in
+             TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xxsrc_r in
            let cdst_r =
-             TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxdst_r in
+             TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xxdst_r in
            let rdefs = [(get_rdef_r xsrc_r); (get_rdef_r xdst_r)] in
            let xprs_r = [xdst_r; xsrc_r; xxdst_r; xxsrc_r] in
            let cxprs_r = [cdst_r; csrc_r] in
@@ -2879,7 +2878,7 @@ object (self)
          let rrhss_rl = List.map (TR.tmap rewrite_expr) rhss_rl in
          let crhss_rl =
            List.map (fun rrhs_r ->
-               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rrhs_r)
+               TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rrhs_r)
              rrhss_rl in
          let (memlhss_rl, cmemlhss_rl, _) =
            List.fold_left
@@ -2887,8 +2886,7 @@ object (self)
                let memop = arm_reg_deref ~with_offset:off basereg WR in
                let memlhs_r = memop#to_variable floc in
                let cmemlhs_r =
-                 TR.tbind
-                   (floc#convert_var_to_c_variable ~size:(Some 4)) memlhs_r in
+                 TR.tbind (floc#var_to_cvar ~size:(Some 4)) memlhs_r in
                (lhss @ [memlhs_r],
                 clhss @ [cmemlhs_r],
                 off + 4)) ([], [], 0) rl#get_register_op_list in
@@ -2904,7 +2902,7 @@ object (self)
                TR.tmap rewrite_expr xaddr_r) in
          let cxaddrs_r =
            List.map (fun xaddr_r ->
-               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xaddr_r)
+               TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xaddr_r)
              xaddrs_r in
          let rdefs = List.map get_rdef_r (baserhs_r :: rrhss_rl) in
          let uses = List.map get_def_use_r (baselhs_r :: memlhss_rl) in
@@ -2967,17 +2965,16 @@ object (self)
 
       | StoreRegister (c, rt, rn, rm, mem, _) ->
          let vmem_r = mem#to_variable floc in
-         let cvmem_r =
-           TR.tbind (floc#convert_var_to_c_variable ~size:(Some 4)) vmem_r in
+         let cvmem_r = TR.tbind (floc#var_to_cvar ~size:(Some 4)) vmem_r in
          let xaddr_r = mem#to_address floc in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrt_r = rt#to_expr floc in
          let xrn_r = rn#to_expr floc in
          let xrm_r = rm#to_expr floc in
          let xxrt_r = TR.tmap rewrite_expr xrt_r in
          let cxrt_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxrt_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) xxrt_r in
          let rdefs =
            [get_rdef_r xrn_r;
             get_rdef_r xrm_r;
@@ -3018,17 +3015,16 @@ object (self)
 
       | StoreRegisterByte (c, rt, rn, rm, mem, _) ->
          let vmem_r = mem#to_variable floc in
-         let cvmem_r =
-           TR.tbind (floc#convert_var_to_c_variable ~size:(Some 1)) vmem_r in
+         let cvmem_r = TR.tbind (floc#var_to_cvar ~size:(Some 1)) vmem_r in
          let xaddr_r = mem#to_address floc in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrt_r = rt#to_expr floc in
          let xrn_r = rn#to_expr floc in
          let xrm_r = rm#to_expr floc in
          let xxrt_r = TR.tmap rewrite_expr xrt_r in
          let cxrt_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 1)) xxrt_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 1)) xxrt_r in
          let rdefs =
            [get_rdef_r xrn_r;
             get_rdef_r xrm_r;
@@ -3156,17 +3152,16 @@ object (self)
 
       | StoreRegisterHalfword (c, rt, rn, rm, mem, _) ->
          let vmem_r = mem#to_variable floc in
-         let cvmem_r =
-           TR.tbind (floc#convert_var_to_c_variable ~size:(Some 2)) vmem_r in
+         let cvmem_r = TR.tbind (floc#var_to_cvar ~size:(Some 2)) vmem_r in
          let xaddr_r = mem#to_address floc in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xrt_r = rt#to_expr floc in
          let xrn_r = rn#to_expr floc in
          let xrm_r = rm#to_expr floc in
          let xxrt_r = TR.tmap rewrite_expr xrt_r in
          let cxrt_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 2)) xxrt_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 2)) xxrt_r in
          let rdefs =
            [get_rdef_r xrn_r;
             get_rdef_r xrm_r;
@@ -3213,7 +3208,7 @@ object (self)
            TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap (rewrite_in_cc_context floc c) result_r in
          let cresult_r =
-           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
+           TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -3676,12 +3671,12 @@ object (self)
          let xbase_r = base#to_expr floc in
          let xaddr_r = mem#to_address floc in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let vmem_r = mem#to_variable floc in
          let xmem_r = mem#to_expr floc in
          let rxbase_r = TR.tmap rewrite_expr xbase_r in
          let rxmem_r = TR.tmap rewrite_expr xmem_r in
-         let cxmem_r = TR.tbind floc#convert_xpr_to_c_expr rxmem_r in
+         let cxmem_r = TR.tbind floc#xpr_to_cxpr rxmem_r in
          let cxmem_r =
            if Result.is_ok cxmem_r then
              cxmem_r
@@ -3692,7 +3687,7 @@ object (self)
                  ~tag:"VLDR:fall-back address conversion"
                  __FILE__ __LINE__
                  ["xxaddr: " ^ (x_r2s xxaddr_r)] in
-             TR.tbind floc#convert_addr_to_c_pointed_to_expr xxaddr_r in
+             TR.tbind floc#addr_to_ctgt_xpr xxaddr_r in
          let rdefs =
            [get_rdef_memvar_r vmem_r; get_rdef_r xmem_r]
            @ (get_all_rdefs_r rxmem_r) in
@@ -3943,11 +3938,10 @@ object (self)
       | VStoreRegister (c, src, base, mem) ->
          let size = src#get_size in
          let vmem_r = mem#to_variable floc in
-         let cvmem_r =
-           TR.tbind (floc#convert_var_to_c_variable ~size:(Some size)) vmem_r in
+         let cvmem_r = TR.tbind (floc#var_to_cvar ~size:(Some size)) vmem_r in
          let xaddr_r = mem#to_address floc in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in
+         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
          let xsrc_r = src#to_expr floc in
          let xbase_r = base#to_expr floc in
          let rxsrc_r = TR.tmap rewrite_expr xsrc_r in