diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-20 23:53:57 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-20 23:53:57 +0200 |
commit | c3c275ebe29d06399ecae84c975d1d21f0d4ed44 (patch) | |
tree | 9158838bd6dcd04524311478bcfb162bcc63da9f /backend | |
parent | 60e4ad85c6cd433c9e28c9e407a957ca3a302c22 (diff) | |
parent | adb864a2a9e607f45e73c518f267264fdb570a19 (diff) | |
download | compcert-kvx-c3c275ebe29d06399ecae84c975d1d21f0d4ed44.tar.gz compcert-kvx-c3c275ebe29d06399ecae84c975d1d21f0d4ed44.zip |
Merge remote-tracking branch 'origin/mppa-cse2' into mppa-cse3
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE2.v | 6 | ||||
-rw-r--r-- | backend/CSE2proof.v | 5 |
2 files changed, 7 insertions, 4 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 => diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 9e0ad909..f9c7b400 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1527,7 +1527,10 @@ Proof. assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. - rewrite (subst_args_ok' sp m); assumption. + - rewrite (subst_args_ok' sp m) by assumption. + eassumption. + - rewrite (subst_arg_ok' sp m) by assumption. + eassumption. } constructor; auto. |