diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:25:48 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:25:48 +0200 |
| commit | 92b48e2aa6d24d1ad487c1d2a3644a57966c765e (patch) | |
| tree | 9ae13a1917a968992338a81a9a4a9fbb62df3222 /mppa_k1c/Asmblockdeps.v | |
| parent | c56f9a47fe1837b7afb73c2c24aed9228bc0db08 (diff) | |
| download | compcert-kvx-92b48e2aa6d24d1ad487c1d2a3644a57966c765e.tar.gz compcert-kvx-92b48e2aa6d24d1ad487c1d2a3644a57966c765e.zip | |
rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 1ee5002c..7cfcbff1 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -135,7 +135,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := let (ge, fn) := Ge in - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with | None => None | Some vl => Some (Val vl) @@ -165,7 +165,7 @@ Definition load_eval (lo: load_op) (l: list value) := Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) := let (ge, fn) := Ge in - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with | None => None | Some m' => Some (Memstate m') @@ -841,7 +841,8 @@ Proof. (* Load Offset *) + destruct i; simpl load_chunk. all: unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + unfold eval_offset; + simpl; auto; destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. @@ -865,7 +866,7 @@ Proof. (* Store Offset *) + destruct i; simpl store_chunk. all: unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + unfold eval_offset; simpl; auto; destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. |