diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:33:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:33:51 +0200 |
| commit | 5b4560bd853cbcf1ef195da1b625f37609ec00ec (patch) | |
| tree | 985a9b244ccb9a9a7b3370f72a841d170ad824c0 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 211382d21013c038c3c716454fcfa5a375dba8ba (diff) | |
| download | compcert-kvx-5b4560bd853cbcf1ef195da1b625f37609ec00ec.tar.gz compcert-kvx-5b4560bd853cbcf1ef195da1b625f37609ec00ec.zip | |
(#139) - Quelques renommages
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2207a2fa..21af276b 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -240,7 +240,7 @@ Lemma exec_basic_instr_pc_var: exec_basic_instr ge i rs m = Next rs' m' -> exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'. Proof. - intros. unfold exec_basic_instr in *. unfold parexec_basic_instr in *. destruct i. + intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i. - unfold exec_arith_instr in *. destruct i; destruct i. all: try (exploreInst; inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). @@ -681,7 +681,7 @@ Lemma transf_exec_basic_instr: forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. Proof. intros. pose symbol_address_preserved. - unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence. + unfold exec_basic_instr. unfold bstep. exploreInst; simpl; auto; try congruence. unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. Qed. |