diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-12 18:38:05 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-12 18:38:05 +0200 |
| commit | 9ba6ffd3346136feef33d400596a3ca89f9e7260 (patch) | |
| tree | e71ab7957ffda1fa31715ed01b8481f7c112b61c /mppa_k1c/Asmblockgenproof.v | |
| parent | 48d4481b6bd246e8912b3d01d98e0bc297f645de (diff) | |
| download | compcert-kvx-9ba6ffd3346136feef33d400596a3ca89f9e7260.tar.gz compcert-kvx-9ba6ffd3346136feef33d400596a3ca89f9e7260.zip | |
Disjonction des cas MB.body bb = nil ou non
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index c89c5177..67974529 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1372,11 +1372,12 @@ Theorem step_simu_body: forall s fb sp bb c ms m rs1 m1 tbb tc ms' m',
body_step ge s fb sp (MB.body bb) ms m ms' m' ->
match_codestate fb (MB.State s fb sp (bb::c) ms m) (Codestate (State rs1 m1) (tbb::tc) (Some tbb)) ->
- exists rs2 m2 tbb',
- exec_straight tge (body tbb) rs1 m1 (body tbb') rs2 m2
+ (mb_remove_body bb = bb \/
+ (exists rs2 m2 tbb',
+ (exec_straight tge (body tbb) rs1 m1 (body tbb') rs2 m2
/\ match_codestate fb (MB.State s fb sp (mb_remove_body bb::c) ms' m')
(Codestate (State rs2 m2) (tbb'::tc) (Some tbb))
- /\ exit tbb' = exit tbb.
+ /\ exit tbb' = exit tbb ))).
Proof.
intros until m'. intros BSTEP MCS. inv BSTEP.
@@ -1409,8 +1410,9 @@ Proof. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. rename tc' into tc.
exploit match_state_codestate; eauto.
intros (S1' & MCS & MAS & cseq). subst.
- exploit step_simu_body; eauto.
- intros (rs2 & m2 & tbb' & EXES & MCS' & Hexit).
+ exploit step_simu_body; eauto. intro STSIMUBODY. inv STSIMUBODY.
+ - (* mb_remove_body bb = bb *) destruct TODO.
+ - destruct H4 as (rs2 & m2 & tbb' & EXES & MCS' & Hexit).
remember (mb_remove_body bb) as bb'.
assert (MB.body bb' = nil).
|