@@ -1499,7 +1499,7 @@ object (self)
14991499 | XConst (IntConst n)
15001500 when n#equal (mkNumerical 0xffffffff ) && is_int t ->
15011501 Ok (int_constant_expr (- 1 ))
1502- | _ -> self#convert_xpr_offsets ~size x
1502+ | _ -> self#convert_xpr_offsets ~xtype ~ size x
15031503
15041504 method convert_addr_to_c_pointed_to_expr
15051505 ?(size =None ) ?(xtype =None ) (a : xpr_t ): xpr_t traceresult =
@@ -1656,12 +1656,13 @@ object (self)
16561656
16571657
16581658 method convert_variable_offsets
1659- ?(size =None ) (v : variable_t ): variable_t traceresult =
1659+ ?(vtype = None ) ?( size =None ) (v : variable_t ): variable_t traceresult =
16601660 if self#env#is_basevar_memory_variable v then
16611661 let basevar_r = self#env#get_memvar_basevar v in
16621662 let offset_r = self#env#get_memvar_offset v in
16631663 let cbasevar_r = TR. tbind self#convert_value_offsets basevar_r in
16641664 let basetype_r = TR. tbind self#get_variable_type cbasevar_r in
1665+ let optvtype = match vtype with Some t -> t | _ -> t_unknown in
16651666 let tgttype_r =
16661667 TR. tbind
16671668 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
@@ -1682,8 +1683,18 @@ object (self)
16821683 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
16831684 (fun tgttype ->
16841685 address_memory_offset
1685- ~tgtsize: size tgttype (num_constant_expr n)) tgttype_r
1686+ ~tgtbtype: optvtype ~tgtsize: size tgttype (num_constant_expr n))
1687+ tgttype_r
16861688 | _ -> Ok offset) offset_r in
1689+ let _ =
1690+ log_diagnostics_result
1691+ ~msg: (p2s self#l#toPretty)
1692+ ~tag: " convert-variable-offsets"
1693+ __FILE__ __LINE__
1694+ [" tgttype: " ^ (TR. tfold_default btype_to_string " ?" tgttype_r);
1695+ " tgtbtype: " ^ (btype_to_string optvtype);
1696+ " offset : " ^ (TR. tfold_default memory_offset_to_string " ?" offset_r);
1697+ " coffset: " ^ (TR. tfold_default memory_offset_to_string " ?" coffset_r)] in
16871698 TR. tbind
16881699 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : " ^ (p2s v#toPretty))
16891700 (fun cbasevar ->
@@ -1776,7 +1787,8 @@ object (self)
17761787 [" v: " ^ (p2s v#toPretty)] in
17771788 Ok v
17781789
1779- method convert_xpr_offsets ?(size =None ) (x : xpr_t ): xpr_t traceresult =
1790+ method convert_xpr_offsets
1791+ ?(xtype =None ) ?(size =None ) (x : xpr_t ): xpr_t traceresult =
17801792 let rec aux exp =
17811793 match exp with
17821794 | XVar v when self#env#is_basevar_memory_value v ->
@@ -1789,10 +1801,16 @@ object (self)
17891801 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
17901802 (fun v -> XVar v) (self#convert_variable_offsets ~size v)
17911803 | XOp ((Xf "addressofvar" ), [XVar v ]) ->
1804+ let derefty =
1805+ match xtype with
1806+ | None -> None
1807+ | Some (TPtr (ty , _ )) -> Some ty
1808+ | _ -> None in
17921809 let newx_r =
17931810 TR. tmap
17941811 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
1795- (fun v -> XVar v) (self#convert_variable_offsets ~size v) in
1812+ (fun v ->
1813+ XVar v) (self#convert_variable_offsets ~vtype: derefty ~size v) in
17961814 TR. tmap
17971815 (fun newx ->
17981816 match newx with
0 commit comments