diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:58 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:58 +0200 |
| commit | 66b506779c4889a18fb7a147f3649005cc40fe7e (patch) | |
| tree | 7fa1332b855741e6c1a34843ec4c7dc9ebfcf325 /backend/CSE2.v | |
| parent | 8532805d67991f25242557124eed009960f6bc61 (diff) | |
| parent | d10bc429a5c08a25471e3f65e328f5cee12e4542 (diff) | |
| download | compcert-kvx-66b506779c4889a18fb7a147f3649005cc40fe7e.tar.gz compcert-kvx-66b506779c4889a18fb7a147f3649005cc40fe7e.zip | |
Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licm
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 8e2307b0..00b1821e 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -276,10 +276,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 @@ -363,7 +363,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 => |