aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE3.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/CSE3.v')
-rw-r--r--backend/CSE3.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v
index 352cc895..2203ad14 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -57,7 +57,7 @@ Definition transf_instr (fmap : 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 =>