diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-02-10 16:26:05 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-02-10 16:26:05 +0100 |
| commit | aec490a064af1cdbcc8ac70a9b5a2c882bea6b55 (patch) | |
| tree | 814c83a1f5835a20b57d2b7cbf5fdf647cc6a9fb /mppa_k1c/Asmblockgenproof.v | |
| parent | 6d3118ad9eec104e8ed0bb86a3f5100d20224fd2 (diff) | |
| download | compcert-kvx-aec490a064af1cdbcc8ac70a9b5a2c882bea6b55.tar.gz compcert-kvx-aec490a064af1cdbcc8ac70a9b5a2c882bea6b55.zip | |
Moved some theorems
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index e130df45..220ae08b 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1353,19 +1353,6 @@ Proof. rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto. Qed. -Lemma exec_body_pc: - forall l rs1 m1 rs2 m2, - exec_body tge l rs1 m1 = Next rs2 m2 -> - rs2 PC = rs1 PC. -Proof. - induction l. - - intros. inv H. auto. - - intros until m2. intro EXEB. - inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate. - eapply IHl in H0. rewrite H0. - erewrite exec_basic_instr_pc; eauto. -Qed. - Lemma exec_body_control: forall b rs1 m1 rs2 m2 rs3 m3 fn, exec_body tge (body b) rs1 m1 = Next rs2 m2 -> |