diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-27 17:49:20 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-27 17:49:20 +0200 |
| commit | 3600b9b62b0deb1c9cc0d3a3d31160144c6aae86 (patch) | |
| tree | d54f9a605041d22c9edd9efca70a5677e8ec663c /mppa_k1c/Asmblockgenproof0.v | |
| parent | 99cb567ffa32366c6d9d7ec5c4f613eac5e71294 (diff) | |
| download | compcert-kvx-3600b9b62b0deb1c9cc0d3a3d31160144c6aae86.tar.gz compcert-kvx-3600b9b62b0deb1c9cc0d3a3d31160144c6aae86.zip | |
storeind_ptr_correct un peu d'avancée
Diffstat (limited to 'mppa_k1c/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index ba2900da..c579cc1a 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -639,8 +639,6 @@ Ltac Simplif := Ltac Simpl := repeat Simplif. -Axiom TODO: False. - Lemma exec_straight_body: forall c rs1 m1 rs2 m2, exec_straight c rs1 m1 nil rs2 m2 -> @@ -650,7 +648,7 @@ Proof. - intros. inv H. - intros. inv H. + inv H7. simpl. remember (exec_basic_instr _ _ _ _) as ebi. destruct ebi; simpl; auto. - + destruct TODO. + + simpl. rewrite H2. apply IHc. auto. Qed. Lemma exec_basic_instr_pc: |