diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 10:34:38 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-10 10:34:38 +0100 |
| commit | 84cb4939653e5355c2039ed62a140aa392e21162 (patch) | |
| tree | 156a6a78208983cf7fca540899313144f36687e0 /riscV/Asmgenproof.v | |
| parent | 3104e551bf87abeab9a257c955cf9b180769dc64 (diff) | |
| download | compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.tar.gz compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.zip | |
[Admitted checker] Checker expansion for reg Ocmp (without scratch)
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 52a3bf27..47ee39f0 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -161,7 +161,7 @@ Proof. Qed. Hint Resolve addptrofs_label: labels. -(* TODO REMOVE Remark transl_cond_float_nolabel: +Remark transl_cond_float_nolabel: forall c r1 r2 r3 insn normal, transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. @@ -173,14 +173,14 @@ Remark transl_cond_single_nolabel: transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. unfold transl_cond_single; intros. destruct c; inv H; exact I. - Qed.*) + Qed. Remark transl_cbranch_label: forall cond args lbl k c, transl_cbranch cond args lbl k = OK c -> tail_nolabel k c. Proof. intros. unfold transl_cbranch in H; destruct cond; TailNoLabel. - (* TODO REMOVE - destruct c0; simpl; TailNoLabel. +- destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - destruct (Int.eq n Int.zero). destruct c0; simpl; TailNoLabel. @@ -211,7 +211,7 @@ Proof. destruct normal; TailNoLabel. - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel.*) + destruct normal; TailNoLabel. - destruct optR0 as [[]|]; TailNoLabel. - destruct optR0 as [[]|]; TailNoLabel. - destruct optR0 as [[]|]; TailNoLabel. @@ -226,7 +226,7 @@ Proof. - destruct optR0 as [[]|]; TailNoLabel. Qed. -(* TODO REMOVE Remark transl_cond_op_label: +Remark transl_cond_op_label: forall cond args r k c, transl_cond_op cond r args k = OK c -> tail_nolabel k c. Proof. @@ -279,7 +279,7 @@ Proof. - destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. destruct normal; TailNoLabel. - Qed.*) + Qed. Remark transl_op_label: forall op args r k c, @@ -303,7 +303,7 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. -(* TODO REMOVE - eapply transl_cond_op_label; eauto.*) +- eapply transl_cond_op_label; eauto. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. |