diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:30 +0200 |
| commit | d10bc429a5c08a25471e3f65e328f5cee12e4542 (patch) | |
| tree | 90d1344259731c9e4ca2552a14092f963b59c95e /backend/CSE3.v | |
| parent | c3c275ebe29d06399ecae84c975d1d21f0d4ed44 (diff) | |
| download | compcert-kvx-d10bc429a5c08a25471e3f65e328f5cee12e4542.tar.gz compcert-kvx-d10bc429a5c08a25471e3f65e328f5cee12e4542.zip | |
forward moves through CSE3 store
Diffstat (limited to 'backend/CSE3.v')
| -rw-r--r-- | backend/CSE3.v | 2 |
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 => |