diff --git a/CodeHawk/CH/chutil/cHLogger.ml b/CodeHawk/CH/chutil/cHLogger.ml
index 82daa9ed..e49e51d9 100644
--- a/CodeHawk/CH/chutil/cHLogger.ml
+++ b/CodeHawk/CH/chutil/cHLogger.ml
@@ -3,7 +3,7 @@
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
+
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny B. Sipma
    Copyright (c) 2021-2025 Aarno Labs LLC
@@ -14,10 +14,10 @@
    to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
    copies of the Software, and to permit persons to whom the Software is
    furnished to do so, subject to the following conditions:
- 
+
    The above copyright notice and this permission notice shall be included in all
    copies or substantial portions of the Software.
-  
+
    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -27,9 +27,9 @@
    SOFTWARE.
    ============================================================================= *)
 
-(** Facility to record problems during a run of the analyzer. 
+(** Facility to record problems during a run of the analyzer.
 
-    Typical use is to catch an exception, record the type of exception thrown 
+    Typical use is to catch an exception, record the type of exception thrown
     with additional data in the logger:
 
     chlog#add "Invalid_Argument" <reason for invalid argument>
@@ -110,17 +110,17 @@ object
 	  tags_discontinued <- tag :: tags_discontinued;
 	  H.replace store tag ((STR "DISCONTINUED") :: entry)
 	end
-      else  
+      else
 	H.replace store tag (msg :: entry)
 
   method reset = H.clear store
 
   method size = H.fold (fun _ v a -> a + (List.length v)) store 0
 
-  method tagsize (tag:string) = 
+  method tagsize (tag:string) =
     if H.mem store tag then List.length (H.find store tag) else 0
 
-  method toPretty = 
+  method toPretty =
     let tags = ref [] in
     let _ = H.iter (fun k _ -> tags := (k, H.find order k) :: !tags) store in
     let tags = List.sort (fun (_, i1) (_, i2) -> Stdlib.compare i2 i1) !tags in
@@ -151,8 +151,8 @@ object
            STR ""); LBLOCK !pp; NL]
 
 end
-      
-    
+
+
 let mk_logger () = new logger_t
 
 let chlog = new logger_t
@@ -252,3 +252,17 @@ let log_result
   chlog#add
     (tag ^ filename ^ ":" ^ (string_of_int linenumber))
     (LBLOCK [STR msg; STR (String.concat "; " error)])
+
+
+let log_diagnostics_result
+      ?(msg="")
+      ?(tag="")
+      (filename: string)
+      (linenumber: int)
+      (msgs: string list) =
+  if collect_diagnostics () then
+    let tag = if tag = "" then tag else tag ^ ":" in
+    let msg = if msg = "" then msg else msg ^ ":" in
+    ch_diagnostics_log#add
+      (tag ^ filename ^ ":" ^ (string_of_int linenumber))
+      (LBLOCK [STR msg; STR (String.concat "; " msgs)])
diff --git a/CodeHawk/CH/chutil/cHLogger.mli b/CodeHawk/CH/chutil/cHLogger.mli
index d6878066..9c9428fa 100644
--- a/CodeHawk/CH/chutil/cHLogger.mli
+++ b/CodeHawk/CH/chutil/cHLogger.mli
@@ -128,3 +128,12 @@ val log_error_result:
     making up [error].*)
 val log_result:
   ?msg:string -> ?tag:string -> string -> int -> string list -> unit
+
+
+(** [log_diagnostics_result msg tag filename linenumber error] writes an entry to
+    [ch_diagnostics_log] with a tag that combines [tag], [filename], and
+    [linenumber].
+    The entry is the concatenation of [msg] and the list of error messages
+    making up [error].*)
+val log_diagnostics_result:
+  ?msg:string -> ?tag:string -> string -> int -> string list -> unit
diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml
index 611d1049..9b5d77cd 100644
--- a/CodeHawk/CH/xprlib/xsimplify.ml
+++ b/CodeHawk/CH/xprlib/xsimplify.ml
@@ -181,6 +181,8 @@ and reduce_bitwise_not (m: bool) (e1: xpr_t): (bool * xpr_t) =
   match e1 with
   | XConst (IntConst num) when num#equal numerical_zero ->
      (true, XConst (IntConst numerical_one#neg))
+  | XConst (IntConst num) when num#equal numerical_one ->
+     (true, XConst (IntConst (mkNumerical 2)#neg))
   | _ -> default ()
 
 
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
index 181f385c..b10225ff 100644
--- a/CodeHawk/CHB/bchlib/bCHFloc.ml
+++ b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -90,6 +90,17 @@ let x2p = xpr_formatter#pr_expr
 let p2s = pretty_to_string
 let x2s x = p2s (x2p x)
 
+let opt_size_to_string (s: int option) =
+  match s with
+  | Some i -> "size:" ^ (string_of_int i)
+  | _ -> "size:None"
+
+let opt_type_to_string (t: btype_t option) =
+  match t with
+  | Some t -> "btype:" ^ (btype_to_string t)
+  | _ -> "btype:None"
+
+
 let log_error (tag: string) (msg: string): tracelogspec_t =
   mk_tracelog_spec ~tag:("floc:" ^ tag) msg
 
@@ -661,61 +672,11 @@ object (self)
               memoffset_r)
         memref_r in
 
-    if self#f#env#is_addressof_symbolic_value var then
-      let xaofv_r = self#f#env#get_addressof_symbolic_expr var in
-      let memvar_r =
-        TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                ^ "var: " ^ (x2s (XVar var)))
-          (fun xaofv ->
-            match xaofv with
-            | XOp ((Xf "addressofvar"), [XVar v]) -> Ok v
-            | _ ->
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                      ^ "Expression is not an addressofvar expression: "
-                      ^ (x2s xaofv)])
-          xaofv_r in
-      let memoff_r =
-        TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-          (fun memvar ->
-            let memtype = self#env#get_variable_type memvar in
-            let memtype =
-              match memtype with
-              | Some t -> t
-              | _ -> t_unknown in
-            address_memory_offset memtype (num_constant_expr numoffset))
-          memvar_r in
-      TR.tbind
-        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-        (fun memvar ->
-          TR.tbind
-            (fun memoff -> self#f#env#add_memory_offset memvar memoff)
-            memoff_r)
-        memvar_r
-
-    else if inv#is_base_offset_constant var then
+    if inv#is_base_offset_constant var then
       let (base, offset) = inv#get_base_offset_constant var in
       let memoffset = numoffset#add offset in
       let memref_r = self#env#mk_base_sym_reference base in
-      let memoff_r =
-        address_memory_offset
-          t_unknown ~tgtsize:(Some size) (num_constant_expr memoffset) in
-      (*
-        To keep representation unifor (i.e., to avoid aliasing) the creation
-        of variable representation against the type of the variable must be
-        delayed until reporting time.
-        TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-          (fun basevar ->
-            let optbasetype = self#env#get_variable_type basevar in
-            let basetype = t_unknown in
-              match optbasetype with
-              | Some t when is_pointer t -> ptr_deref t
-              | _ -> t_unknown in
-            address_memory_offset t_unknown
-              ~tgtsize:(Some size) (num_constant_expr memoffset))
-          (self#env#get_variable base#getSeqNumber) in *)
+      let memoff_r = Ok (ConstantOffset (memoffset, NoOffset)) in
       mk_memvar memref_r memoff_r
 
     else
@@ -902,15 +863,6 @@ object (self)
       (fun memref ->
         if memref#is_global_reference then
           self#get_var_at_address ~size:(Some size) address
-      (*
-          TR.tbind
-            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
-            (fun memoff ->
-              TR.tbind
-                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-                (self#env#mk_global_variable ~size)
-                (get_total_constant_offset memoff))
-            memoff_r *)
         else
           TR.tbind
             ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
@@ -963,33 +915,6 @@ object (self)
           (get_total_constant_offset memoffset)
     else
       default ()
-        (*
-      match memoffset with
-      | IndexOffset _ ->
-         self#env#mk_offset_memory_variable memref memoffset
-      | ConstantOffset (n, IndexOffset (v, s, o)) ->
-         let n = n#modulo (mkNumerical BCHDoubleword.e32) in
-         log_tfold_default
-           (mk_tracelog_spec
-              ~tag:"get_memory_variable_3"
-              (self#cia
-               ^ ": constant: "
-               ^ n#toString
-               ^ "; index-expr: "
-               ^ "; offset: "
-               ^ offset#toString
-               ^ (x2s indexExpr)
-               ^ "; addr: "
-               ^ (x2s addr)
-               ^ "; memoffset: "
-               ^ (memory_offset_to_string memoffset)))
-           (fun v -> v)
-           (default ())
-           (self#env#mk_index_offset_global_memory_variable
-              n (IndexOffset (v, s, o)))
-      | _ ->
-         default ()
-         *)
 
   (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    * resolve and save ScaledReg (None,indexreg, scale, offset)
@@ -1404,6 +1329,10 @@ object (self)
                                ^ (btype_to_string basevartype)
                                ^ " not yet handled"])
                    symmemoff_r
+              | FieldOffset ((fname, ckey), NoOffset) ->
+                 let cinfo = get_compinfo_by_key ckey in
+                 let finfo = get_compinfo_field cinfo fname in
+                 Ok finfo.bftype
               | _ ->
                  Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
                         ^ "memoff: " ^ (memory_offset_to_string memoff)
@@ -1433,6 +1362,169 @@ object (self)
                 ^ "variable: " ^ (x2s (XVar v))]
       | Some t -> Ok t
 
+  method convert_xpr_to_c_expr
+           ?(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"
+        __FILE__ __LINE__
+        [(opt_size_to_string size) ^ "; "
+         ^ (opt_type_to_string 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 ~size x
+
+  method convert_addr_to_c_pointed_to_expr
+           ?(size=None) ?(xtype=None) (a: xpr_t): xpr_t traceresult =
+    let vars = vars_as_positive_terms a in
+    let knownpointers =
+      List.filter (fun v ->
+          (self#f#is_base_pointer v)
+          || (TR.tfold_default is_pointer false (self#get_variable_type v))
+        ) 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) -> Ok (ConstantOffset (n, NoOffset))
+         | _ ->
+            Error [__FILE__ ^ ":" ^ (string_of_int __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__))
+           (fun memref memoff ->
+             self#env#mk_offset_memory_variable memref memoff)
+           memref_r memoff_r in
+       TR.tmap (fun v -> XVar v) var_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
+       let var_r =
+         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 in
+       TR.tmap (fun v -> XVar v) var_r
+    | _ ->
+       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+              ^ (opt_size_to_string size) ^ "; "
+              ^ (opt_type_to_string xtype) ^ "; "
+              ^ "addr: " ^ (x2s a)
+              ^ ": Not yet handled"]
+
+  method convert_var_to_c_variable
+           ?(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__) ^ ": "
+              ^ (opt_size_to_string size) ^ "; "
+              ^ (opt_type_to_string 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) -> 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__) ^ ": "
+              ^ (opt_size_to_string size) ^ "; "
+              ^ (opt_type_to_string vtype) ^ "; "
+              ^ "addr: " ^ (x2s a)
+              ^ ": Not yet handled"]
+
+
   method convert_variable_offsets
            ?(size=None) (v: variable_t): variable_t traceresult =
     if self#env#is_basevar_memory_variable v then
@@ -1471,6 +1563,12 @@ object (self)
             ) coffset_r)
         cbasevar_r
     else
+      let _ =
+        log_diagnostics_result
+          ~msg:(p2s self#l#toPretty)
+          ~tag:"convert-variable-offsets:default"
+          __FILE__ __LINE__
+          [(p2s v#toPretty)] in
       Ok v
 
   method convert_value_offsets
@@ -1478,7 +1576,11 @@ object (self)
     if self#env#is_basevar_memory_value v then
       let basevar_r = self#env#get_memval_basevar v in
       let offset_r = self#env#get_memval_offset v in
-      let cbasevar_r = TR.tbind self#convert_value_offsets basevar_r in
+      let cbasevar_r =
+        TR.tbind
+          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+          (self#convert_value_offsets ~size)
+          basevar_r in
       let basetype_r = TR.tbind self#get_variable_type cbasevar_r in
       let tgttype_r =
         TR.tbind
@@ -1486,6 +1588,11 @@ object (self)
           (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__) ^ ": "
+                      ^ "Target type is a struct: " ^ cinfo.bcname
+                      ^ ". A pointer was expected"]
             | t ->
                Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
                       ^ "Type " ^ (btype_to_string t)
@@ -1496,6 +1603,12 @@ object (self)
           (fun offset ->
             match offset with
             | NoOffset ->
+               let _ =
+                 log_diagnostics_result
+                   ~msg:(p2s self#l#toPretty)
+                   ~tag:"convert-value-offsets:NoOffset"
+                   __FILE__ __LINE__
+                   ["v: " ^ (p2s v#toPretty)] in
                TR.tbind
                  ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
                  (fun tgttype ->
@@ -1512,13 +1625,25 @@ object (self)
         ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))
         (fun cbasevar ->
           TR.tbind
+            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                  ^ "cbasevar: " ^ (p2s cbasevar#toPretty))
             (fun coffset ->
               let memvar_r =
                 self#env#mk_basevar_memory_variable cbasevar coffset in
-              TR.tbind self#env#mk_initial_memory_value memvar_r
+              TR.tbind
+                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                      ^ "cbasevar: " ^ (p2s cbasevar#toPretty)
+                      ^ "; coffset: " ^ (memory_offset_to_string coffset))
+                self#env#mk_initial_memory_value memvar_r
             ) coffset_r)
         cbasevar_r
     else
+      let _ =
+        log_diagnostics_result
+          ~msg:(p2s self#l#toPretty)
+          ~tag:"convert-value-offsets:default"
+          __FILE__ __LINE__
+          ["v: " ^ (p2s v#toPretty)] in
       Ok v
 
   method convert_xpr_offsets ?(size=None) (x: xpr_t): xpr_t traceresult =
@@ -1526,7 +1651,8 @@ object (self)
       match exp with
       | XVar v when self#env#is_basevar_memory_value v ->
          TR.tmap
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           ~msg:(__FILE__ ^ ":" ^ (string_of_int __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
@@ -1546,7 +1672,14 @@ object (self)
       | XOp (op, [xx]) -> TR.tmap (fun x -> XOp (op, [x])) (aux xx)
       | XOp (op, [x1; x2]) ->
          TR.tmap2 (fun x1 x2 -> XOp (op, [x1; x2])) (aux x1) (aux x2)
-      | _ -> Ok exp in
+      | _ ->
+         let _ =
+           log_diagnostics_result
+             ~msg:(p2s self#l#toPretty)
+             ~tag:"convert-xpr-offsets:default"
+             __FILE__ __LINE__
+             ["x: " ^ (x2s x) ^ "; exp: " ^ (x2s exp)] in
+         Ok exp in
     aux x
 
   method get_xpr_type (x: xpr_t): btype_t traceresult =
@@ -1566,51 +1699,15 @@ object (self)
     | [base] (* when self#f#env#is_initial_stackpointer_value base *) ->
        let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
        let memref_r = self#env#mk_base_variable_reference base in
-       let memoff_r = address_memory_offset t_unknown offset in
-       (memref_r, memoff_r)
-
-       (* resolving to type-based representations at this point may give
-          rise to aliasing; for example __ptr_deref_R[0]_in.field_4 may be aliased
-          with R[0]_in[4]_in
-    | [base] ->
-       let offset = simplify_xpr (XOp (XMinus, [x; 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 x) ^ "; base: " ^ (x2s (XVar base))
-                      ^ "; offset: " ^ (x2s offset)])
-           rvartype_r in
+       (* let memoff_r = address_memory_offset t_unknown offset 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
-        *)
-
-       (*
-         (match offset with
-          | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
-          | XOp (XMult, [XConst (IntConst n); XVar v]) ->
-             Ok (IndexOffset (v, n#toInt, NoOffset))
-          | _ ->
-             Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                    ^ "Offset from base "
-                    ^ (x2s (XVar base))
-                    ^ " not recognized: " ^ (x2s offset)]) in *)
-    (* (memref_r, memoff_r) *)
+         match offset with
+         | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
+         | _ ->
+            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                   ^ "base: " ^ (p2s base#toPretty)
+                   ^ "; offset expr: " ^ (x2s offset)] in
+       (memref_r, memoff_r)
 
     (* no known pointers, have to find a base *)
     | [] ->
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index 976b6a75..8863bf68 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -3338,6 +3338,15 @@ type memory_offset_t =
       that the type of the variable is known). The index expression must
       consist solely of constants or constant-value variables.*)
 
+  | BasePtrArrayIndexOffset of xpr_t * memory_offset_t
+  (** index expression is scaled by the size of the target type of the base
+      pointer (assumes the target type of the base pointer is known. This
+      case is distinct from the ArrayIndexOffset in that the pointer variable
+      must be dereferenced first to access the element, while in the case of
+      an array the access is immediate. In CIL these two types of array accesses
+      have different representation.
+   *)
+
   | UnknownOffset
   (** used if none of the above apply *)
 
@@ -5931,6 +5940,24 @@ 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
 
diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml
index 27473f45..773c3857 100644
--- a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml
+++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml
@@ -86,6 +86,8 @@ let rec memory_offset_to_string offset =
       (memory_offset_to_string subOffset)
   | ArrayIndexOffset (x, subOffset) ->
      "[" ^ (x2s x) ^  "]" ^ (memory_offset_to_string subOffset)
+  | BasePtrArrayIndexOffset (x, subOffset) ->
+     "[<[" ^ (x2s x) ^ "]>]" ^ (memory_offset_to_string subOffset)
   | UnknownOffset -> "?offset?"
 
 
@@ -134,6 +136,14 @@ let rec memory_offset_compare (o1: memory_offset_t) (o2: memory_offset_t) =
        l1
   | (ArrayIndexOffset _, _) -> -1
   | (_, ArrayIndexOffset _) -> 1
+  | (BasePtrArrayIndexOffset (x1, so1), BasePtrArrayIndexOffset (x2, so2)) ->
+     let l1 = syntactic_comparison x1 x2 in
+     if l1 = 0 then
+       memory_offset_compare so1 so2
+     else
+       l1
+  | (BasePtrArrayIndexOffset _, _) -> -1
+  | (_, BasePtrArrayIndexOffset _) -> 1
   | (UnknownOffset, UnknownOffset) -> 0
 
 
@@ -155,8 +165,8 @@ let rec mk_maximal_memory_offset (n: numerical_t) (ty: btype_t): memory_offset_t
        UnknownOffset
   else if is_array_type ty then
     ConstantOffset (n, NoOffset)
-  else if n#equal numerical_zero then
-    NoOffset
+  (* else if n#equal numerical_zero then
+    NoOffset *)
   else
     begin
       ch_error_log#add
@@ -175,16 +185,18 @@ let rec address_memory_offset
           ?(tgtbtype=t_unknown)
           (basetype: btype_t)
           (xoffset: xpr_t): memory_offset_t traceresult =
+  let iszero x =
+    match x with
+    | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero
+    | _ -> false in
   let rbasetype = TR.tvalue (resolve_type basetype) ~default:t_unknown in
   match xoffset with
-  | XConst (IntConst n)
-       when n#equal CHNumerical.numerical_zero
-            && Option.is_none tgtsize
-            && is_unknown_type tgtbtype -> Ok NoOffset
-  | XConst (IntConst n)
-       when n#equal CHNumerical.numerical_zero && is_unknown_type rbasetype ->
-     Ok NoOffset
   | XConst (IntConst n) when is_unknown_type rbasetype ->
+     let _ =
+       log_diagnostics_result
+         ~msg:"address-memory-offset:unknown basetype"
+         __FILE__ __LINE__
+         ["xoffset: " ^ n#toString] in
      Ok (ConstantOffset (n, NoOffset))
   | XConst (IntConst n) ->
      let tgtbtype =
@@ -194,7 +206,14 @@ let rec address_memory_offset
      else if is_array_type rbasetype then
        arrayvar_memory_offset ~tgtsize ~tgtbtype rbasetype xoffset
      else
-       Ok (ConstantOffset (n, NoOffset))
+       let _ =
+         log_diagnostics_result
+           ~msg:"address-memory-offset:scalar basetype"
+           __FILE__ __LINE__
+           ["base type: " ^ (btype_to_string rbasetype)
+            ^ "; xoffset: " ^ n#toString] in
+       (* Ok (ConstantOffset (n, NoOffset)) *)
+       Ok (BasePtrArrayIndexOffset (num_constant_expr n, NoOffset))
   | _ ->
      let tgtbtype =
        if is_unknown_type tgtbtype then None else Some tgtbtype in
@@ -203,10 +222,22 @@ let rec address_memory_offset
      else if is_array_type rbasetype then
        arrayvar_memory_offset ~tgtsize ~tgtbtype rbasetype xoffset
      else
-       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ "Offset " ^ (x2s xoffset) ^ " with base type "
-              ^ (btype_to_string rbasetype)
-              ^ " not yet supported"]
+       let tsize_r = size_of_btype rbasetype in
+       TR.tbind
+         (fun tsize ->
+           let optindex = BCHXprUtil.get_array_index_offset xoffset tsize in
+           match optindex with
+           | None ->
+              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                     ^ "Unable to extract index from " ^ (x2s xoffset)]
+           | Some (indexxpr, xrem) when iszero xrem ->
+              Ok (BasePtrArrayIndexOffset (indexxpr, NoOffset))
+           | _ ->
+              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                     ^ "Nonzero suboffset encountered when extracting index "
+                     ^ "from " ^ (x2s xoffset) ^ " with base type "
+                     ^ (btype_to_string rbasetype)])
+         tsize_r
 
 and structvar_memory_offset
 ~(tgtsize: int option)
@@ -214,11 +245,6 @@ and structvar_memory_offset
 (btype: btype_t)
 (xoffset: xpr_t): memory_offset_t traceresult =
   match xoffset with
-  | XConst (IntConst n) when
-         n#equal CHNumerical.numerical_zero
-         && Option.is_none tgtsize
-         && Option.is_none tgtbtype ->
-     Ok NoOffset
   | XConst (IntConst _) ->
      if is_struct_type btype then
        let compinfo = get_struct_type_compinfo btype in
@@ -248,54 +274,47 @@ and arrayvar_memory_offset
     | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero
     | _ -> false in
 
-  match xoffset with
-  | XConst (IntConst n) when
-         n#equal CHNumerical.numerical_zero
-         && Option.is_none tgtsize
-         && Option.is_none tgtbtype ->
-     Ok NoOffset
-  | _ ->
-     if is_array_type btype then
-       let eltty = get_element_type btype in
-       TR.tbind
-       ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-         (fun elsize ->
-           let optindex = BCHXprUtil.get_array_index_offset xoffset elsize in
-           match optindex with
-           | None ->
-              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                     ^ "Unable to extract index from " ^ (x2s xoffset)]
-           | Some (indexxpr, xrem) when
-                  iszero xrem
-                  && Option.is_none tgtsize
-                  && Option.is_none tgtbtype ->
-              Ok (ArrayIndexOffset (indexxpr, NoOffset))
-           | Some (indexxpr, rem) ->
-              if (TR.tfold_default is_struct_type false (resolve_type eltty)) then
-                let eltty = TR.tvalue (resolve_type eltty) ~default:t_unknown in
-                TR.tbind
-                  ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-                  (fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
-                  (structvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
-              else if is_array_type eltty then
-                TR.tbind
-                  ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-                  (fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
-                  (arrayvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
-              else if is_scalar eltty then
-                let x2index = XOp (XDiv, [rem; int_constant_expr elsize]) in
-                let x2index = Xsimplify.simplify_xpr x2index in
-                Ok (ArrayIndexOffset (x2index, NoOffset))
-              else
-                Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                       ^ "xoffset: " ^ (x2s xoffset)
-                       ^ "; btype: " ^ (btype_to_string btype)
-                       ^ "; elementtype: " ^ (btype_to_string eltty)])
-         (size_of_btype eltty)
-     else
-       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
-              ^ " xoffset: " ^ (x2s xoffset)
-              ^ "; btype: " ^ (btype_to_string btype)]
+  if is_array_type btype then
+    let eltty = get_element_type btype in
+    TR.tbind
+      ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+      (fun elsize ->
+        let optindex = BCHXprUtil.get_array_index_offset xoffset elsize in
+        match optindex with
+        | None ->
+           Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                  ^ "Unable to extract index from " ^ (x2s xoffset)]
+        | Some (indexxpr, xrem) when
+               iszero xrem
+               && Option.is_none tgtsize
+               && Option.is_none tgtbtype ->
+           Ok (ArrayIndexOffset (indexxpr, NoOffset))
+        | Some (indexxpr, rem) ->
+           if (TR.tfold_default is_struct_type false (resolve_type eltty)) then
+             let eltty = TR.tvalue (resolve_type eltty) ~default:t_unknown in
+             TR.tbind
+               ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+               (fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
+               (structvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
+           else if is_array_type eltty then
+             TR.tbind
+               ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+               (fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
+               (arrayvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
+           else if is_scalar eltty then
+             let x2index = XOp (XDiv, [rem; int_constant_expr elsize]) in
+             let x2index = Xsimplify.simplify_xpr x2index in
+             Ok (ArrayIndexOffset (x2index, NoOffset))
+           else
+             Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                    ^ "xoffset: " ^ (x2s xoffset)
+                    ^ "; btype: " ^ (btype_to_string btype)
+                    ^ "; elementtype: " ^ (btype_to_string eltty)])
+      (size_of_btype eltty)
+  else
+    Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
+           ^ " xoffset: " ^ (x2s xoffset)
+           ^ "; btype: " ^ (btype_to_string btype)]
 
 
 and get_field_memory_offset_at
@@ -429,6 +448,12 @@ let rec is_field_offset (offset: memory_offset_t): bool =
   | _ -> false
 
 
+let is_base_ptr_array_index_offset (offset: memory_offset_t): bool =
+  match offset with
+  | BasePtrArrayIndexOffset (_, suboffset) -> is_constant_offset suboffset
+  | _ -> false
+
+
 let rec is_index_offset (offset: memory_offset_t): bool =
   match offset with
   | IndexOffset (_, _, NoOffset) -> true
@@ -461,14 +486,6 @@ let rec get_constant_offsets
          __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
          ^ "Offset is not constant: "
          ^ (memory_offset_to_string offset)]
-       (*
-     raise
-       (BCH_failure
-          (LBLOCK [
-               STR __FILE__; STR ":"; INT __LINE__; STR ": ";
-               STR "offset ";
-               STR (memory_offset_to_string offset);
-               STR " is not constant"])) *)
 
 
 let rec add_offset
@@ -479,6 +496,8 @@ let rec add_offset
   | FieldOffset (f, o) -> FieldOffset (f, add_offset o offset2)
   | IndexOffset (v, i, o) -> IndexOffset (v, i, add_offset o offset2)
   | ArrayIndexOffset (x, o) -> ArrayIndexOffset (x, add_offset o offset2)
+  | BasePtrArrayIndexOffset (x, o) ->
+     BasePtrArrayIndexOffset (x, add_offset o offset2)
   | UnknownOffset -> UnknownOffset
 
 
diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.mli b/CodeHawk/CHB/bchlib/bCHMemoryReference.mli
index 04042dee..77724ec1 100644
--- a/CodeHawk/CHB/bchlib/bCHMemoryReference.mli
+++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.mli
@@ -101,6 +101,9 @@ val is_field_offset: memory_offset_t -> bool
 val is_index_offset: memory_offset_t -> bool
 
 
+val is_base_ptr_array_index_offset: memory_offset_t -> bool
+
+
 (** Returns [true] if [memoff] itself or one of its suboffsets is an unknown
     offset. *)
 val is_unknown_offset: memory_offset_t -> bool
diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
index ec62f370..6f19a95a 100644
--- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
+++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
@@ -642,9 +642,10 @@ object
     | FieldOffset _ -> "f"
     | IndexOffset _ -> "i"
     | ArrayIndexOffset _ -> "a"
+    | BasePtrArrayIndexOffset _ -> "p"
     | UnknownOffset -> "u"
 
-  method !tags = ["a"; "c"; "f"; "i"; "n"; "u"]
+  method !tags = ["a"; "c"; "f"; "i"; "n"; "p"; "u"]
 end
 
 let memory_offset_mcts: memory_offset_t mfts_int = new memory_offset_mcts_t
diff --git a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml
index af90df97..5359fc30 100644
--- a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml
+++ b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml
@@ -150,6 +150,8 @@ object (self)
          (tags, [xd#index_variable v; i; self#index_memory_offset m])
       | ArrayIndexOffset (x, m) ->
          (tags, [xd#index_xpr x; self#index_memory_offset m])
+      | BasePtrArrayIndexOffset (x, m) ->
+         (tags, [xd#index_xpr x; self#index_memory_offset m])
       | UnknownOffset -> (tags,[]) in
     memory_offset_table#add key
 
@@ -166,6 +168,7 @@ object (self)
     | "i" ->
        IndexOffset (xd#get_variable (a 0), a 1, self#get_memory_offset (a 2))
     | "a" -> ArrayIndexOffset (xd#get_xpr (a 0), self#get_memory_offset (a 1))
+    | "p" -> BasePtrArrayIndexOffset (xd#get_xpr (a 0), self#get_memory_offset (a 1))
     | "u" -> UnknownOffset
     | s -> raise_tag_error name s memory_offset_mcts#tags
 
diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml
index 0a18cc42..a9a8d99d 100644
--- a/CodeHawk/CHB/bchlib/bCHVariable.ml
+++ b/CodeHawk/CHB/bchlib/bCHVariable.ml
@@ -1006,7 +1006,10 @@ object (self)
   method has_constant_offset (v: variable_t) =
     (self#is_memory_variable v)
     && (tfold_default
-          (fun off -> is_constant_offset off || is_field_offset off)
+          (fun off ->
+            (is_constant_offset off)
+            || (is_field_offset off)
+            || (is_base_ptr_array_index_offset off))
           false
           (self#get_memvar_offset v))
 
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 0dc5da81..60d791e5 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_20250316"
-  ~date:"2025-03-14"
+  ~version:"0.6.0_20250401"
+  ~date:"2025-04-01"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
index c7720b36..d804228f 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
@@ -288,7 +288,7 @@ let cc_expr
        (XOp (XGt, [v x; v y]), [x; y])
 
     | (LogicalShiftLeft (true, ACCAlways, _, x, y, _), ACCNonNegative) ->
-      (XOp (XGe, [XOp (XLsl, [vu x; vu y]); zero_constant_expr]), [x; y])
+       (XOp (XGe, [XOp (XLsl, [vu x; vu y]); zero_constant_expr]), [x; y])
 
     (* ------------------------------------------------- Compare-negative --- *)
 
@@ -310,8 +310,11 @@ let cc_expr
 
     (* ------------------------------------------------------------- Move --- *)
 
-    | (Move (true, ACCAlways, _, y, _, _), ACCNotEqual) ->
-       (XOp (XNe, [v y; zero_constant_expr]), [y])
+    | (Move (true, ACCAlways, _, x, _, _), ACCEqual) ->
+       (XOp (XEq, [v x; zero_constant_expr]), [x])
+
+    | (Move (true, ACCAlways, _, x, _, _), ACCNotEqual) ->
+       (XOp (XNe, [v x; zero_constant_expr]), [x])
 
     (* ------------------------------------------------- Reverse Subtract --- *)
 
@@ -344,6 +347,9 @@ let cc_expr
     | (Subtract (true, ACCAlways, _, x, y, _, _), ACCNegative) ->
        (XOp (XLt, [XOp (XMinus, [v x; v y]); zero_constant_expr]), [x; y])
 
+    | (Subtract (true, ACCAlways, _, x, y, _, _), ACCNonNegative) ->
+       (XOp (XGe, [XOp (XMinus, [v x; v y]); zero_constant_expr]), [x; y])
+
     | (Subtract (true, ACCAlways, _, x, y, _, _), ACCNotEqual) ->
        (XOp (XNe, [XOp (XMinus, [v x; v y]); zero_constant_expr]), [x; y])
 
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml
index 411ebd54..660a750a 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml
@@ -614,6 +614,10 @@ object (self:'a)
        let vreg = floc#env#mk_arm_register_variable r in
        let shiftv = XOp (XBAnd, [XVar vsreg; int_constant_expr 7]) in
        Ok (XOp (XLsl, [XVar vreg; shiftv]))
+    | ARMShiftedReg (r, ARMRegSRT (SRType_LSR, sr)) ->
+       let vsreg = floc#env#mk_arm_register_variable sr in
+       let vreg = floc#env#mk_arm_register_variable r in
+       Ok (XOp (XLsr, [XVar vreg; XVar vsreg]))
     | ARMShiftedReg (_, srt) ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
               ^ "Shifted reg: " ^ (register_shift_to_string srt)
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
index 0114cd90..8142dcce 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
@@ -78,6 +78,8 @@ module TR = CHTraceResult
 
 let x2p = xpr_formatter#pr_expr
 let p2s = CHPrettyUtil.pretty_to_string
+let x2s x = p2s (x2p x)
+let x_r2s x_r = TR.tfold_default x2s "error-value" x_r
 
 let log_error (tag: string) (msg: string): tracelogspec_t =
   mk_tracelog_spec ~tag:("FnARMDictionary:" ^ tag) msg
@@ -362,19 +364,23 @@ object (self)
                (LBLOCK [
                     STR __FILE__; STR ":"; INT __LINE__; STR ": ";
                     STR "Empty tag list"])) in
-      let xtag = (List.hd tags) ^ "vtlxdh" in
+      let xtag = (List.hd tags) ^ "vtlxcdh" in
       let uses = [get_def_use_r v] in
       let useshigh = [get_def_use_high_r v] in
       let argslen = List.length args in
       let vbutag = "vbu:" ^ (string_of_int argslen) in
       let xbutag = "xbu:" ^ (string_of_int (argslen + 3)) in
-      let tags = xtag :: ((List.tl tags) @ [vbutag; xbutag]) in
+      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 args =
         args
         @ [index_variable v;
            bcd#index_typ t_unknown;
            inc;
-           index_xpr x]
+           index_xpr x;
+           index_xpr cx]
         @ uses @ useshigh in
       (tags, args) in
 
@@ -382,7 +388,8 @@ object (self)
           (tags: string list)
           (args: int list)
           (rv: xpr_t traceresult)
-          (rrv: xpr_t traceresult): (string list) * (int list) =
+          (rrv: xpr_t traceresult)
+          (crv: xpr_t traceresult): (string list) * (int list) =
       let _ =
         if (List.length tags) = 0 then
           raise
@@ -391,11 +398,11 @@ object (self)
                     STR __FILE__; STR ":"; INT __LINE__; STR ": ";
                     STR "Empty tag list"])) in
       let rdefs = [get_rdef_r rv] @ (get_all_rdefs_r rrv) in
-      let xtag = (List.hd tags) ^ "xx" ^ (string_repeat "r" (List.length rdefs)) in
+      let xtag = (List.hd tags) ^ "xxc" ^ (string_repeat "r" (List.length rdefs)) in
       let argslen = List.length args in
       let returntag = "return:" ^ (string_of_int argslen) in
       let tags = xtag :: ((List.tl tags) @ [returntag]) in
-      let args = args @ [index_xpr rv; index_xpr rrv] @ rdefs in
+      let args = args @ [index_xpr rv; index_xpr rrv; index_xpr crv] @ rdefs in
       (tags, args)in
 
     let mk_instrx_data
@@ -458,8 +465,10 @@ object (self)
 
     let mk_instrx_data_r
           ?(vars_r: variable_t traceresult list = [])
+          ?(cvars_r: variable_t traceresult list = [])
           ?(types: btype_t list = [])
           ?(xprs_r: xpr_t traceresult list = [])
+          ?(cxprs_r: xpr_t traceresult list = [])
           ?(rdefs: int list = [])
           ?(uses: int list = [])
           ?(useshigh: int list = [])
@@ -469,15 +478,19 @@ object (self)
         if testsupport#requested_instrx_data then
           testsupport#submit_instrx_data instr#get_address vars_r xprs_r in
       let varcount = List.length vars_r in
+      let cvarcount = List.length cvars_r in
       let xprcount = List.length xprs_r in
+      let cxprcount = List.length cxprs_r in
       let rdefcount = List.length rdefs in
       let defusecount = List.length uses in
       let defusehighcount = List.length useshigh in
       let flagrdefcount = List.length flagrdefs in
       let integercount = List.length integers in
       let varstring = string_repeat "v" varcount in
+      let cvarstring = string_repeat "w" cvarcount in
       let typestring = string_repeat "t" varcount in
       let xprstring = string_repeat "x" xprcount in
+      let cxprstring = string_repeat "c" cxprcount in
       let rdefstring = string_repeat "r" rdefcount in
       let defusestring = string_repeat "d" defusecount in
       let defusehighstring = string_repeat "h" defusehighcount in
@@ -486,15 +499,19 @@ object (self)
       let tagstring =
         "ar:"
         ^ varstring
+        ^ cvarstring
         ^ typestring
         ^ xprstring
+        ^ cxprstring
         ^ rdefstring
         ^ defusestring
         ^ defusehighstring
         ^ flagrdefstring
         ^ integerstring in
       let varargs = List.map index_variable vars_r in
+      let cvarargs = List.map index_variable cvars_r in
       let xprargs = List.map index_xpr xprs_r in
+      let cxprargs = List.map index_xpr cxprs_r in
       let typeargs =
         let types =
           if (List.length types) < varcount then
@@ -504,8 +521,10 @@ object (self)
         List.map bcd#index_typ types in
       (tagstring,
        varargs
+       @ cvarargs
        @ typeargs
        @ xprargs
+       @ cxprargs
        @ rdefs
        @ uses
        @ useshigh
@@ -603,8 +622,8 @@ object (self)
     let callinstr_key (): (string list * int list) =
       let callargs = floc#get_call_arguments in
       let _ = check_for_functionptr_args callargs in
-      let (xprs, xvars, rdefs, _) =
-        List.fold_left (fun (xprs, xvars, rdefs, index) (p, x) ->
+      let (xprs, cxprs_r, xvars, rdefs, _) =
+        List.fold_left (fun (xprs, cxprs_r, xvars, rdefs, index) (p, x) ->
             let xvar_r =
               if is_register_parameter p then
                 let regarg = TR.tget_ok (get_register_parameter_register p) in
@@ -636,10 +655,14 @@ object (self)
                         (floc#get_var_at_address ~btype:(ptr_deref ptype) xx)
               else
                 xx in
-            let xx = TR.tvalue (floc#convert_xpr_offsets xx) ~default:xx in
+            let cx_r = floc#convert_xpr_to_c_expr ~xtype:(Some ptype) xx in
             let rdef = get_rdef_r xvar_r in
-            (xx :: xprs, xvar_r :: xvars, rdef :: rdefs, index + 1))
-          ([], [], [], 1) callargs in
+            (xx :: xprs,
+             cx_r :: cxprs_r,
+             xvar_r :: xvars,
+             rdef :: rdefs,
+             index + 1))
+          ([], [], [], [], 1) callargs in
       let (vrd, rtype) =
         let fintf = floc#get_call_target#get_function_interface in
         let rtype = get_fts_returntype fintf in
@@ -663,15 +686,16 @@ object (self)
             let rdefs = get_all_rdefs x in
             let newixs = List.filter (fun ix -> not (List.mem ix acc)) rdefs in
             acc @ newixs) [] xprs in
+      let vars_r = [Ok vrd] in
+      let xprs_r = (List.rev (List.map (fun x -> Ok x) xprs)) @ (List.rev xvars) in
+      let cxprs_r = List.rev cxprs_r in
+      let types = [rtype] in
+      let rdefs = (List.rev rdefs) @ xrdefs in
+      let uses = [get_def_use vrd] in
+      let useshigh = [get_def_use_high vrd] in
       let (tagstring, args) =
         mk_instrx_data_r
-          ~vars_r:[Ok vrd]
-          ~types:[rtype]
-          ~xprs_r:((List.rev (List.map (fun x -> Ok x) xprs)) @ (List.rev xvars))
-          ~rdefs:((List.rev rdefs) @ xrdefs)
-          ~uses:[get_def_use vrd]
-          ~useshigh:[get_def_use_high vrd]
-          () in
+          ~vars_r ~types ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
       let tags =
         if instr#is_inlined_call then
           tagstring :: ["call"; "inlined"]
@@ -716,36 +740,26 @@ object (self)
          let xxrn_r = TR.tmap rewrite_expr xrn_r in
          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
          let _ =
            TR.tfold_default
              (fun r -> ignore (get_string_reference floc r)) () 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
-         let useshigh = get_def_use_high_r vrd_r in
          let vrtype =
            match get_regvar_type_annotation () with
            | Some t -> t
            | _ -> t_unknown in
-         (*
-         let rresult_r =
-           TR.tmap
-             (fun rresult ->
-               TR.tfold_default
-                 (fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
-                 rresult
-                 (floc#get_var_at_address rresult))
-             rresult_r in
-          *)
+         let uses = [get_def_use_r vrd_r] in
+         let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let types = [vrtype] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~types:[vrtype]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r]
-             ~rdefs:rdefs
-             ~uses:[uses]
-             ~useshigh:[useshigh]
-             () in
+             ~vars_r ~types ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let tags = add_optional_subsumption tags in
          (tags, args)
@@ -777,18 +791,18 @@ object (self)
       | Adr (c, rd, imm) ->
          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
          let _ =
            TR.tfold_default
              (fun x -> ignore (get_string_reference floc x)) () ximm_r in
-         let uses = get_def_use_r vrd_r in
-         let useshigh = get_def_use_high_r vrd_r in
+         let uses = [get_def_use_r vrd_r] in
+         let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [ximm_r] in
+         let cxprs_r = [caddr_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[ximm_r]
-             ~uses:[uses]
-             ~useshigh:[useshigh]
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let tags = add_optional_subsumption tags in
          (tags, args)
@@ -806,18 +820,17 @@ object (self)
                | _ -> XOp (XAsr, [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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let tags = add_optional_subsumption tags in
          (tags, args)
@@ -864,18 +877,17 @@ object (self)
          let result_r =
            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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -888,18 +900,18 @@ object (self)
              (fun xrn xrm -> XOp (XBAnd, [xrn; XOp (XBNot, [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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+             ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -910,18 +922,17 @@ object (self)
          let result_r =
            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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -930,17 +941,17 @@ object (self)
          let xrm_r = rm#to_expr floc in
          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
          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
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+             ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -951,18 +962,16 @@ 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 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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let _ =
            TR.tfold_default
              (fun r -> ignore (get_string_reference floc r)) () rresult_r  in
@@ -1063,32 +1072,38 @@ object (self)
          let csetter = floc#f#get_associated_cc_setter floc#cia in
          let tcond = rewrite_test_expr csetter txpr in
          let fcond = rewrite_test_expr csetter fxpr in
-         let tcond_r = floc#convert_xpr_offsets ~size:(Some 4) tcond in
-         let fcond_r = floc#convert_xpr_offsets ~size:(Some 4) fcond 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 csetter_addr_r = string_to_doubleword csetter in
+         let csetter_instr_r =
+           TR.tbind get_arm_assembly_instruction csetter_addr_r in
          let bytestr =
-           try
-             let instr =
-               fail_tvalue
-                 (trerror_record
-                    (LBLOCK [STR "Internal error in FnARMDictionary:Branch"]))
-                 (get_arm_assembly_instruction
-                    (fail_tvalue
-                       (trerror_record
-                          (LBLOCK [STR "FnARMDictionary:Branch: "; STR csetter]))
-                       (string_to_doubleword csetter))) in
-             instr#get_bytes_ashexstring
-           with
-           | _ -> "0x0" in
+           TR.tfold
+             ~ok:(fun instr -> instr#get_bytes_ashexstring)
+             ~error:(fun e ->
+               begin log_error_result __FILE__ __LINE__ e; "0x0" end)
+             csetter_instr_r in
          let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in
-         let (tagstring, args) =
-           mk_instrx_data_r
-             ~xprs_r:[Ok txpr; Ok fxpr; tcond_r; fcond_r; xtgt_r]
-             ~rdefs
-             () in
+         let xprs_r = [Ok txpr; Ok fxpr; Ok tcond; Ok fcond; xtgt_r] in
+         let cxprs_r = [ctcond_r; cfcond_r] in
+         let (tagstring, args) = mk_instrx_data_r ~xprs_r ~cxprs_r ~rdefs () in
          let (tags, args) = (tagstring :: ["TF"; csetter; bytestr], args) in
          let tags = add_optional_subsumption tags in
          (tags, args)
 
+      (* conditional branch without test expression *)
+      | Branch (c, tgt, _)
+           when is_cond_conditional c
+                && tgt#is_absolute_address ->
+         let xtgt_r = tgt#to_expr floc in
+         let xxtgt_r = TR.tmap rewrite_expr xtgt_r in
+         let xprs_r = [xtgt_r; xxtgt_r] in
+         let rdefs = (get_rdef_r xtgt_r) :: (get_all_rdefs_r xxtgt_r) in
+         let (tagstring, args) = mk_instrx_data_r ~xprs_r ~rdefs () in
+         let (tags, args) = (tagstring :: ["TF:no-x"], args) in
+         let tags = add_optional_subsumption tags in
+         (tags, args)
+
       | Branch (_, tgt, _) ->
          let xtgt_r = tgt#to_expr floc in
          let xxtgt_r = TR.tmap rewrite_expr xtgt_r in
@@ -1103,9 +1118,10 @@ object (self)
          let r0_op = arm_register_op AR0 RD in
          let xr0_r = r0_op#to_expr floc in
          let xxr0_r = TR.tmap rewrite_expr xr0_r in
+         let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr 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 in
+         let (tags, args) = add_return_value tags args xr0_r xxr0_r cxr0_r in
          (tags, args)
 
       | BranchExchange (c, tgt) ->
@@ -1179,12 +1195,14 @@ object (self)
          let xresult_r =
            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 result_r =
-           TR.tbind (floc#convert_xpr_offsets ~size:(Some 4)) result_r in
+         let cresult_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~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
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r ~xprs_r:[xrn_r; xrm_r; result_r] ~rdefs () in
+           mk_instrx_data_r ~xprs_r ~cxprs_r ~rdefs () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let tags = add_optional_subsumption tags in
          (tags, args)
@@ -1407,32 +1425,41 @@ object (self)
          let baselhs_r = base#to_variable floc in
          let baserhs_r = base#to_expr floc in
          let regcount = rl#get_register_count in
-         let (rhsexprs_r, _) =
+         let (memrhss_r, rmemrhss_r, cmemrhss_r, _) =
            List.fold_left
-             (fun (acc, off) _lhsvar ->
+             (fun (mems, rmems, cmems, off) _lhsvar ->
                let memop = arm_reg_deref ~with_offset:off basereg RD in
                let memrhs_r = memop#to_expr floc in
-               (acc @ [memrhs_r], off + 4)) ([], 0) lhsvars_rl 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
+               (mems @ [memrhs_r],
+                rmems @ [rmemrhs_r],
+                cmems @ [cmemrhs_r],
+                off + 4)) ([], [], [], 0) lhsvars_rl in
          let xaddrs_r =
            List.init
              rl#get_register_count
              (fun i ->
                let xaddr_r =
                  TR.tmap
-                   (fun baserhs -> XOp (XPlus, [baserhs; int_constant_expr (i + 4)]))
+                   (fun baserhs ->
+                     XOp (XPlus, [baserhs; int_constant_expr (i + 4)]))
                    baserhs_r in
                TR.tmap rewrite_expr xaddr_r) in
-         let rdefs = List.map get_rdef_r (baserhs_r :: rhsexprs_r) in
+         let cxaddrs_r =
+           List.map (fun xaddr_r ->
+               TR.tbind (floc#convert_xpr_to_c_expr ~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
          let useshigh = List.map get_def_use_high_r (baselhs_r :: lhsvars_rl) in
+         let vars_r = baselhs_r :: lhsvars_rl in
+         let xprs_r = baserhs_r :: (memrhss_r @ rmemrhss_r @ xaddrs_r) in
+         let cxprs_r = cmemrhss_r @ cxaddrs_r in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:(baselhs_r :: lhsvars_rl)
-             ~xprs_r:(baserhs_r :: (rhsexprs_r @ xaddrs_r))
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+             ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let tags = add_optional_subsumption tags in
          let (tags, args) =
@@ -1517,9 +1544,20 @@ 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 xrmem_r = TR.tmap rewrite_expr xmem_r in
-         let xrmem_r =
-           TR.tbind (floc#convert_xpr_offsets ~size:(Some 4)) xrmem_r in
+         let cxrmem_r = TR.tbind floc#convert_xpr_to_c_expr xrmem_r in
+         let cxrmem_r =
+           if Result.is_ok cxrmem_r then
+             cxrmem_r
+           else
+             let _ =
+               log_diagnostics_result
+                 ~msg:(p2s floc#l#toPretty)
+                 ~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
          let _ =
            TR.tfold_default
              (fun xrmem -> ignore (get_string_reference floc xrmem)) () xrmem_r in
@@ -1532,8 +1570,9 @@ object (self)
              ~vtype:t_unknown in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vrt_r; vmem_r]
-             ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xaddr_r]
+             ~vars_r:[vrt_r]
+             ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xaddr_r; xxaddr_r]
+             ~cxprs_r:[cxrmem_r; cxaddr_r]
              ~rdefs
              ~uses
              ~useshigh
@@ -1723,14 +1762,21 @@ object (self)
          let xaddr_r = mem#to_address floc in
          let vmem_r = mem#to_variable floc in
          let xmem_r = mem#to_expr floc in
-         let xrmem_r = TR.tmap rewrite_expr xmem_r in
-         let xrmem_r = TR.tbind floc#convert_xpr_offsets xrmem_r in
-         let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r; get_rdef_memvar_r vmem_r]
            @ (get_all_rdefs_r xmem_r) in
          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 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
+         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
          let _ =
            floc#memrecorder#record_load_r
              ~signed:false
@@ -1740,8 +1786,9 @@ object (self)
              ~vtype:t_unknown in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vrt_r; vmem_r]
-             ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xaddr_r]
+             ~vars_r:[vrt_r]
+             ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xaddr_r; xxaddr_r]
+             ~cxprs_r:[cxrmem_r; cxaddr_r]
              ~rdefs
              ~uses
              ~useshigh
@@ -1969,21 +2016,21 @@ object (self)
          let vrd_r = rd#to_variable floc in
          let xrm_r = rm#to_expr floc in
          let result_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) xrm_r in
+         let cresult_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~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
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrm_r; result_r] in
+         let cxprs_r = [cresult_r] in
          let _ =
            TR.tfold_default
              (fun result -> ignore (get_string_reference floc result))
              () result_r in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrm_r; result_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+             ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -2043,18 +2090,17 @@ object (self)
          let result_r =
            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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -2159,7 +2205,8 @@ object (self)
              let r0_op = arm_register_op AR0 RD in
              let xr0_r = r0_op#to_expr floc in
              let xxr0_r = TR.tmap rewrite_expr xr0_r in
-             add_return_value tags args xr0_r xxr0_r
+             let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr xxr0_r in
+             add_return_value tags args xr0_r xxr0_r cxr0_r
            else
              (tags, args) in
          (tags, args)
@@ -2223,18 +2270,17 @@ object (self)
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrm; xrn])) 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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -2554,11 +2600,14 @@ object (self)
            let xdst_r = dstop#to_expr floc in
            let xxsrc_r = TR.tmap (rewrite_floc_expr srcfloc) xsrc_r in
            let xxdst_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) xdst_r in
-           let xxdst_r =
-             TR.tmap
-               (fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
-               (TR.tbind floc#get_var_at_address xxdst_r) in
+           let csrc_r =
+             TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxsrc_r in
+           let cdst_r =
+             TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xdst_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
+           let integers = [size] in
            let _ =
              TR.tfold_default
                (fun xxsrc ->
@@ -2568,11 +2617,7 @@ object (self)
                ()
                xxsrc_r in
            let (tagstring, args) =
-             mk_instrx_data_r
-               ~xprs_r:[xdst_r; xsrc_r; xxdst_r; xxsrc_r]
-               ~integers:[size]
-               ~rdefs
-               () in
+             mk_instrx_data_r ~xprs_r ~cxprs_r ~integers ~rdefs () in
            let tags = tagstring :: ["agg-ldmstm"] in
            let tags = add_subsumption_dependents agg tags in
            (tags, args)
@@ -2590,33 +2635,56 @@ object (self)
          let regcount = rl#get_register_count in
          let rhss_rl = rl#to_multiple_expr floc in
          let rrhss_rl = List.map (TR.tmap rewrite_expr) rhss_rl in
-         let (memlhss_rl, _) =
+         let crhss_rl =
+           List.map (fun rrhs_r ->
+               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rrhs_r)
+             rrhss_rl in
+         let (memlhss_rl, cmemlhss_rl, _) =
            List.fold_left
-             (fun (acc, off) _reg ->
+             (fun (lhss, clhss, off) _reg ->
                let memop = arm_reg_deref ~with_offset:off basereg WR in
                let memlhs_r = memop#to_variable floc in
-               (acc @ [memlhs_r], off + 4)) ([], 0) rl#get_register_op_list in
+               let cmemlhs_r =
+                 TR.tbind
+                   (floc#convert_var_to_c_variable ~size:(Some 4)) memlhs_r in
+               (lhss @ [memlhs_r],
+                clhss @ [cmemlhs_r],
+                off + 4)) ([], [], 0) rl#get_register_op_list in
+         let xaddrs_r =
+           List.init
+             rl#get_register_count
+             (fun i ->
+               let xaddr_r =
+                 TR.tmap
+                   (fun baserhs ->
+                     XOp (XPlus, [baserhs; int_constant_expr (i + 4)]))
+                   baserhs_r in
+               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)
+             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
          let useshigh = List.map get_def_use_high_r (baselhs_r :: memlhss_rl) in
-         let wbackresults_r =
+         let vars_r = baselhs_r :: memlhss_rl in
+         let cvars_r = cmemlhss_rl in
+         let xprs_r = (baserhs_r :: rhss_rl) @ rrhss_rl @ xaddrs_r in
+         let cxprs_r = crhss_rl @ cxaddrs_r in
+         let (tagstring, args) =
+           mk_instrx_data_r
+             ~vars_r ~cvars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
+         let (tags, args) = add_optional_instr_condition tagstring args c in
+         let (tags, args) =
            if wback then
-             let increm = int_constant_expr (4 * regcount) in
+             let inc = 4 * regcount in
+             let xinc = int_constant_expr inc in
              let baseresult_r =
-               TR.tmap (fun baserhs -> XOp (XPlus, [baserhs; increm])) baserhs_r in
+               TR.tmap (fun baserhs -> XOp (XPlus, [baserhs; xinc])) baserhs_r in
              let rbaseresult_r = TR.tmap rewrite_expr baseresult_r in
-             [baseresult_r; rbaseresult_r]
+             add_base_update tags args baselhs_r inc rbaseresult_r
            else
-             [baserhs_r; baserhs_r] in
-         let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:(baselhs_r :: memlhss_rl)
-             ~xprs_r:((baserhs_r :: wbackresults_r) @ rrhss_rl)
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
-         let (tags, args) = add_optional_instr_condition tagstring args c in
+             (tags, args) in
          (tags, args)
 
       | StoreMultipleIncrementBefore (wback, c, base, rl, _) ->
@@ -2631,11 +2699,6 @@ object (self)
              (fun (acc, off) _reg ->
                let memop = arm_reg_deref ~with_offset:off basereg WR in
                let memlhs_r = memop#to_variable floc in
-               let memlhs_r =
-                 let r =
-                   TR.tbind
-                     (floc#convert_variable_offsets ~size:(Some 4)) memlhs_r in
-                 if Result.is_ok r then r else memlhs_r in
                (acc @ [memlhs_r], off + 4)) ([], 4) rl#get_register_op_list 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
@@ -2662,17 +2725,17 @@ object (self)
 
       | StoreRegister (c, rt, rn, rm, mem, _) ->
          let vmem_r = mem#to_variable floc in
-         let vmem_r =
-           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem_r in
-           if Result.is_ok r then r else vmem_r in
+         let cvmem_r =
+           TR.tbind (floc#convert_var_to_c_variable ~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 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 xxrtc_r = TR.tbind floc#convert_xpr_offsets xxrt_r in
-         let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let lhsvar_r = TR.tbind floc#get_var_at_address xxaddr_r in
+         let cxrt_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxrt_r in
          let rdefs =
            [get_rdef_r xrn_r;
             get_rdef_r xrm_r;
@@ -2680,8 +2743,10 @@ object (self)
             get_rdef_r xxrt_r] in
          let uses = [get_def_use_r vmem_r] in
          let useshigh = [get_def_use_high_r vmem_r] in
-         let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xxrtc_r; xaddr_r] in
-         let vars_r = [vmem_r; lhsvar_r] in
+         let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r; xxaddr_r] in
+         let cxprs_r = [cxrt_r; cxaddr_r] in
+         let vars_r = [vmem_r] in
+         let cvars_r = [cvmem_r] in
          let _ =
            floc#memrecorder#record_store_r
              ~addr_r:xxaddr_r
@@ -2690,7 +2755,8 @@ object (self)
              ~vtype:t_unknown
              ~xpr_r:xxrt_r in
          let (tagstring, args) =
-           mk_instrx_data_r ~vars_r ~xprs_r ~rdefs ~uses ~useshigh () in
+           mk_instrx_data_r
+             ~vars_r ~cvars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let (tags, args) =
            if mem#is_offset_address_writeback then
@@ -2710,17 +2776,17 @@ object (self)
 
       | StoreRegisterByte (c, rt, rn, rm, mem, _) ->
          let vmem_r = mem#to_variable floc in
-         let vmem_r =
-           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 1)) vmem_r in
-           if Result.is_ok r then r else vmem_r in
+         let cvmem_r =
+           TR.tbind (floc#convert_var_to_c_variable ~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 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 xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let lhsvar_r =
-           TR.tbind (floc#get_var_at_address ~size:(Some 1)) xxaddr_r in
+         let cxrt_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 1)) xxrt_r in
          let rdefs =
            [get_rdef_r xrn_r;
             get_rdef_r xrm_r;
@@ -2728,6 +2794,10 @@ object (self)
             get_rdef_r xxrt_r] in
          let uses = [get_def_use_r vmem_r] in
          let useshigh = [get_def_use_high_r vmem_r] in
+         let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r; xxaddr_r] in
+         let cxprs_r = [cxrt_r; cxaddr_r] in
+         let vars_r = [vmem_r] in
+         let cvars_r = [cvmem_r] in
          let _ =
            floc#memrecorder#record_store_r
              ~addr_r:xxaddr_r
@@ -2737,14 +2807,9 @@ object (self)
              ~xpr_r:xxrt_r in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vmem_r; lhsvar_r]
-             ~xprs_r:[xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+             ~vars_r ~cvars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
-                  let (tags, args) =
+         let (tags, args) =
            if mem#is_offset_address_writeback then
              let vrn_r = rn#to_variable floc in
              TR.tfold
@@ -2762,13 +2827,7 @@ object (self)
 
       | StoreRegisterDual (c, rt, rt2, rn, rm, mem, mem2) ->
          let vmem_r = mem#to_variable floc in
-         let vmem_r =
-           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem_r in
-           if Result.is_ok r then r else vmem_r in
          let vmem2_r = mem2#to_variable floc in
-         let vmem2_r =
-           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem2_r in
-           if Result.is_ok r then r else vmem2_r in
          let xaddr1_r = mem#to_address floc in
          let xaddr2_r = mem2#to_address floc in
          let xaddr1_r = TR.tmap rewrite_expr xaddr1_r in
@@ -2855,16 +2914,17 @@ object (self)
 
       | StoreRegisterHalfword (c, rt, rn, rm, mem, _) ->
          let vmem_r = mem#to_variable floc in
-         let vmem_r =
-           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 2)) vmem_r in
-           if Result.is_ok r then r else vmem_r in
+         let cvmem_r =
+           TR.tbind (floc#convert_var_to_c_variable ~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 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 xxrt_r = TR.tbind floc#convert_xpr_offsets xxrt_r in
-         let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
+         let cxrt_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 2)) xxrt_r in
          let rdefs =
            [get_rdef_r xrn_r;
             get_rdef_r xrm_r;
@@ -2872,6 +2932,10 @@ object (self)
             get_rdef_r xxrt_r] in
          let uses = [get_def_use_r vmem_r] in
          let useshigh = [get_def_use_high_r vmem_r] in
+         let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r; xxaddr_r] in
+         let cxprs_r = [cxrt_r; cxaddr_r] in
+         let vars_r = [vmem_r] in
+         let cvars_r = [cvmem_r] in
          let _ =
            floc#memrecorder#record_store_r
              ~addr_r:xxaddr_r
@@ -2881,12 +2945,7 @@ object (self)
              ~xpr_r:xxrt_r in
          let (tagstring, args) =
            mk_instrx_data_r
-             ~vars_r:[vmem_r]
-             ~xprs_r:[xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+             ~vars_r ~cvars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          let (tags, args) =
            if mem#is_offset_address_writeback then
@@ -2911,18 +2970,20 @@ object (self)
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XMinus, [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
          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
          let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs
-             ~uses
-             ~useshigh
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
+         let _ =
+           TR.tfold_default
+             (fun r -> ignore (get_string_reference floc r)) () rresult_r  in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
index cf87b0f6..17701e49 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -74,6 +74,7 @@ module TR = CHTraceResult
 let x2p = xpr_formatter#pr_expr
 let p2s = CHPrettyUtil.pretty_to_string
 let x2s x = p2s (x2p x)
+let x_r2s x_r = TR.tfold_default x2s "error-value" x_r
 
 let log_error (tag: string) (msg: string): tracelogspec_t =
   mk_tracelog_spec ~tag:("TranslateARMToCHIF:" ^ tag) msg
@@ -2256,7 +2257,13 @@ let translate_arm_instruction
   | Pop (c, sp, rl, _) ->
      let floc = get_floc loc in
      let regcount = rl#get_register_count in
-
+     let is_restore_temporary (r: register_t) =
+       if rl#includes_pc then
+         match r with
+         | ARMRegister armreg -> List.mem armreg arm_temporaries
+         | _ -> false
+       else
+         false in
      let popcmds (): cmd_t list =
        let sprhs_r = sp#to_expr floc in
        let regs = rl#to_multiple_register in
@@ -2271,7 +2278,21 @@ let translate_arm_instruction
              let cmds1 = floc#get_assign_commands_r (Ok reglhs) stackrhs_r in
              let usevars =
                TR.tfold_default (fun stackvar -> [stackvar]) [] stackvar_r in
-             let usehigh = get_use_high_vars_r ~is_pop:true [stackrhs_r] in
+             let usehigh =
+               if is_restore_temporary reg then
+                 let _ =
+                   chlog#add
+                     "register restore of temporary"
+                     (LBLOCK [
+                          floc#l#toPretty;
+                          STR ": ";
+                          STR (register_to_string reg);
+                          STR " := ";
+                          STR (x_r2s (TR.tmap (rewrite_expr floc) stackrhs_r))
+                     ]) in
+                 []
+               else
+                 get_use_high_vars_r ~is_pop:true [stackrhs_r] in
              let defcmds1 =
                floc#get_vardef_commands
                  ~defs:[reglhs; splhs]
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/CRYPTO_malloc.xml b/CodeHawk/CHB/bchsummaries/so_functions/CRYPTO_malloc.xml
deleted file mode 100644
index 6e1be71f..00000000
--- a/CodeHawk/CHB/bchsummaries/so_functions/CRYPTO_malloc.xml
+++ /dev/null
@@ -1,54 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<codehawk-binary-analyzer>
-  <header date="2021-12-26 18:13:30"/>
-  <libfun lib="so_functions" name="CRYPTO_malloc">
-    <documentation>
-      <desc>
-	OPENSSL_malloc(), OPENSSL_realloc(), and OPENSSL_free() are
-	like the C malloc(), realloc(), and free()
-	functions. OPENSSL_zalloc() calls memset() to zero the memory
-	before returning.
-
-	OpenSSL memory allocation is handled by the OPENSSL_xxx
-	API. These are generally macro's that add the standard C
-	__FILE__ and __LINE__ parameters and call a lower-level
-	CRYPTO_xxx API. Some functions do not add those parameters,
-	but exist for consistency.
-      </desc>
-      <apidoc>
-        <pt>
-          <ll>void *CRYPTO_malloc(</ll>
-          <ld>size_t num</ld>
-          <ld>char *file</ld>
-          <ld>int line</ld>
-          <ll>)</ll>
-        </pt>
-        <par name="num">number of bytes to allocate</par>
-        <par name="file">name of the source file</par>
-        <par name="line">source line number</par>
-        <return>
-          <rc cond="success">not null</rc>
-          <rc cond="failure">null</rc>
-        </return>
-      </apidoc>
-    </documentation>
-    <api adj="0" cc="cdecl" name="CRYPTO_malloc">
-      <par loc="stack" name="num" nr="1">
-        <type>size_t</type>
-      </par>
-      <par loc="stack" name="file" nr="2">
-        <type><ptr>char</ptr></type>
-      </par>
-      <par loc="stack" name="line" nr="3">
-        <type>int</type>
-      </par>
-      <returntype><ptr>void</ptr></returntype>
-    </api>
-    <semantics>
-      <io-actions/>
-      <preconditions/>
-      <postconditions/>
-      <sideeffects/>
-    </semantics>
-  </libfun>
-</codehawk-binary-analyzer>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/RAND_bytes.xml b/CodeHawk/CHB/bchsummaries/so_functions/RAND_bytes.xml
deleted file mode 100644
index c4627be4..00000000
--- a/CodeHawk/CHB/bchsummaries/so_functions/RAND_bytes.xml
+++ /dev/null
@@ -1,41 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<codehawk-binary-analyzer>
-  <header date="2021-12-26 18:23:08"/>
-  <libfun lib="so_functions" name="RAND_bytes">
-    <documentation>
-      <desc>
-	generates num random bytes using a cryptographically secure
-	pseudo random generator (CSPRNG) and stores them in buf.
-      </desc>
-      <apidoc>
-        <pt>
-          <ll>int RAND_bytes(</ll>
-          <ld>char *buf</ld>
-          <ld>int num</ld>
-          <ll>)</ll>
-        </pt>
-        <par name="buf">buffer to store the random sequence</par>
-        <par name="num">number of bytes to generate</par>
-        <return>
-          <rc cond="success">1</rc>
-          <rc cond="failure">-1 or 0</rc>
-        </return>
-      </apidoc>
-    </documentation>
-    <api adj="0" cc="cdecl" name="RAND_bytes">
-      <par loc="stack" name="buf" nr="1">
-        <type><ptr>char</ptr></type>
-      </par>
-      <par loc="stack" name="num" nr="2">
-        <type>int</type>
-      </par>
-      <returntype>int</returntype>
-    </api>
-    <semantics>
-      <io-actions/>
-      <preconditions/>
-      <postconditions/>
-      <sideeffects/>
-    </semantics>
-  </libfun>
-</codehawk-binary-analyzer>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml b/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml
index f13c638e..3eb86121 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml
@@ -24,7 +24,7 @@
     </apidoc>
    </documentation>
    <api adj="0" cc="cdecl" name="gmtime">
-     <returntype><ptr>gmtime</ptr></returntype>
+     <returntype><ptr>ch_tm</ptr></returntype>
      <par loc="stack" io="r" name="timer" nr="1">
      <roles>
        <role rt="ioc:memops" rn="src-bytes:time_t" />
diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml
index 9ffa6d23..df0fcc82 100644
--- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml
+++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml
@@ -91,7 +91,7 @@ let translate_store () =
       ("STRDwb1", "0x1b4bc", "f0416de100",
        [("var_0016", "R4_in");
         ("var_0012", "R5_in");
-        ("SP", "sv__15__sv")]);
+        ("SP", "sv__23__sv")]);
       ("STRDwb2", "0x10ab8", "fc406de100",
        [("var_0012", "R4_in");
         ("var_0008", "R5_in");