diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-06 15:54:56 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-06 15:54:56 +0100 |
| commit | 3811d877943c0724dc3abf03709849942e912aa9 (patch) | |
| tree | a1e71beceb1416dced360a707bc312b2158450ab /mppa_k1c/Asmblockgenproof0.v | |
| parent | 9e2184dc81f6375140114208bd8a2db89b905d38 (diff) | |
| download | compcert-kvx-3811d877943c0724dc3abf03709849942e912aa9.tar.gz compcert-kvx-3811d877943c0724dc3abf03709849942e912aa9.zip | |
MBcond true proved (but a small change needs to be done to Asmblockgenproof1)
Diffstat (limited to 'mppa_k1c/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 3db0c2cd..6a71a746 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -815,6 +815,21 @@ Proof. rewrite <- H7. simpl. rewrite H1. auto. Qed. +Lemma exec_straight_body2: + forall c rs1 m1 c' rs2 m2, + exec_straight c rs1 m1 c' rs2 m2 -> + exists body, + exec_body ge body rs1 m1 = Next rs2 m2 + /\ (basics_to_code body) ++g c' = c. +Proof. + intros until m2. induction 1. + - exists (i1::nil). split; auto. simpl. rewrite H. auto. + - destruct IHexec_straight as (bdy & EXEB & BTC). + exists (i:: bdy). split; simpl. + + rewrite H. auto. + + congruence. +Qed. + (* Lemma exec_straight_body2: forall c c' l rs1 m1 rs2 m2, exec_straight (c++c') rs1 m1 c' rs2 m2 -> |