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/CSE3analysisproof.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/CSE3analysisproof.v')
-rw-r--r-- | backend/CSE3analysisproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f4ec7a10..e1e9f6cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -848,14 +848,14 @@ Section SOUNDNESS. Qed. Hint Resolve store1_sound : cse3. - + Theorem store_sound: forall no chunk addr args a src rel tenv rs m m', sem_rel rel rs m -> wt_regset tenv rs -> eval_addressing genv sp addr (rs ## args) = Some a -> Mem.storev chunk m a (rs#src) = Some m' -> - sem_rel (store (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + sem_rel (store (ctx:=ctx) no chunk addr args src (tenv (forward_move (ctx:=ctx) rel src)) rel) rs m'. Proof. unfold store. intros until m'. @@ -863,8 +863,8 @@ Section SOUNDNESS. rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. apply store1_sound with (a := a) (m := m); trivial. - rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. - assumption. + (* rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + assumption. *) Qed. Hint Resolve store_sound : cse3. |