diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 09:32:37 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 09:32:37 +0200 |
| commit | d193a67519e6aae60fcc31905714e5ed5dc828d0 (patch) | |
| tree | d26ff3366c05391f4e572b943d50fd554600be96 /mppa_k1c/Asmblockdeps.v | |
| parent | c73ab51128c8fdbac327292f46cab289dd69fee5 (diff) | |
| download | compcert-kvx-d193a67519e6aae60fcc31905714e5ed5dc828d0.tar.gz compcert-kvx-d193a67519e6aae60fcc31905714e5ed5dc828d0.zip | |
merged
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 77cc02e4..a9f14f8e 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -916,8 +916,7 @@ Proof. destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ] eqn:MEML0; simpl. ++ destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ] eqn:MEML1. - +++ rewrite H0. - rewrite H. + +++ rewrite H. rewrite MEML0. rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). rewrite H0. @@ -945,14 +944,14 @@ Proof. **** rewrite (assign_diff _ (#rd0) (#r) _) by (apply ppos_discr; apply not_eq_sym; assumption). rewrite Pregmap.gso by assumption. trivial. - +++ rewrite H0. rewrite H. rewrite MEML0. + +++ rewrite H. rewrite MEML0. rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). rewrite H0. rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). rewrite H. rewrite MEML1. constructor. - ++ rewrite H0. rewrite H. rewrite MEML0. trivial. + ++ rewrite H. rewrite MEML0. trivial. (* Load Octuple word *) + unfold parexec_load_o_offset. |