From adb864a2a9e607f45e73c518f267264fdb570a19 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Apr 2020 23:51:53 +0200 Subject: forward moves into store source --- backend/CSE2.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index d9fe5799..dabbaa22 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -389,10 +389,10 @@ Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := | Some bf => rel | None => kill_mem rel end - | EF_malloc (* FIXME *) + | EF_malloc (* would need lessdef *) | EF_external _ _ | EF_vstore _ - | EF_free (* FIXME *) + | EF_free (* would need lessdef? *) | EF_memcpy _ _ (* FIXME *) | EF_inline_asm _ _ _ => kill_mem rel | _ => rel @@ -476,7 +476,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) | Some src => Iop Omove (src::nil) dst s end | Istore chunk addr args src s => - Istore chunk addr (subst_args fmap pc args) src s + Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s | Icall sig ros args dst s => Icall sig ros (subst_args fmap pc args) dst s | Itailcall sig ros args => -- cgit