File tree Expand file tree Collapse file tree 1 file changed +19
-2
lines changed
Expand file tree Collapse file tree 1 file changed +19
-2
lines changed Original file line number Diff line number Diff line change @@ -685,7 +685,14 @@ object (self)
685685 | XVar _ -> xx
686686 | _ ->
687687 TR. tfold
688- ~ok: (fun v -> XOp ((Xf " addressofvar" ), [(XVar v)]))
688+ ~ok: (fun v ->
689+ let _ =
690+ log_diagnostics_result
691+ ~msg: (p2s floc#l#toPretty)
692+ ~tag: " callinstr-key:get-var-at-address"
693+ __FILE__ __LINE__
694+ [" xx: " ^ (x2s xx); " v: " ^ (p2s v#toPretty)] in
695+ XOp ((Xf " addressofvar" ), [(XVar v)]))
689696 ~error: (fun e ->
690697 let _ = log_dc_error_result __FILE__ __LINE__ e in
691698 xx)
@@ -2787,10 +2794,20 @@ object (self)
27872794 let xdst_r = dstop#to_expr floc in
27882795 let xxsrc_r = TR. tmap (rewrite_floc_expr srcfloc) xsrc_r in
27892796 let xxdst_r = TR. tmap (rewrite_expr ?restrict:(Some 4 )) xdst_r in
2797+ let xxdst_r =
2798+ TR. tmap
2799+ (fun x ->
2800+ TR. tfold
2801+ ~ok: (fun v -> XOp ((Xf " addressofvar" ), [(XVar v)]))
2802+ ~error: (fun e ->
2803+ let _ = log_dc_error_result __FILE__ __LINE__ e in
2804+ x)
2805+ (floc#get_var_at_address ~btype: t_int x))
2806+ xxdst_r in
27902807 let csrc_r =
27912808 TR. tbind (floc#convert_xpr_to_c_expr ~size: (Some 4 )) xxsrc_r in
27922809 let cdst_r =
2793- TR. tbind (floc#convert_xpr_to_c_expr ~size: (Some 4 )) xdst_r in
2810+ TR. tbind (floc#convert_xpr_to_c_expr ~size: (Some 4 )) xxdst_r in
27942811 let rdefs = [(get_rdef_r xsrc_r); (get_rdef_r xdst_r)] in
27952812 let xprs_r = [xdst_r; xsrc_r; xxdst_r; xxsrc_r] in
27962813 let cxprs_r = [cdst_r; csrc_r] in
You can’t perform that action at this time.
0 commit comments