diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 15:44:20 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 15:44:20 +0200 |
| commit | 5ffa8534d09272e5f44c51193e74cffdbc2b043c (patch) | |
| tree | c391ce9fa363db667a36775c8cf56a6e6f484ed0 /backend/Duplicateproof.v | |
| parent | bd4fbff2badea3922bf0e144777ae8ecfdc30e74 (diff) | |
| download | compcert-kvx-5ffa8534d09272e5f44c51193e74cffdbc2b043c.tar.gz compcert-kvx-5ffa8534d09272e5f44c51193e74cffdbc2b043c.zip | |
Icond
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index aa605bea..ba1fecc1 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -127,6 +127,15 @@ Proof. destruct (builtin_res_eq_pos _ _); try discriminate. eapply verify_is_copy_correct_one. destruct x. eassumption. subst. constructor. +(* Icond *) + - destruct i'; try (inversion H; fail). monadInv H. + unfold verify_is_copy in EQ, EQ1. + destruct (_ ! n1) eqn:REVM; [|inversion EQ]. + destruct (n ?= p) eqn:NP; try (inversion EQ; fail). eapply Pos.compare_eq in NP. subst. inv EQ. + destruct (_ ! n2) eqn:REVMM; [|inversion EQ1]. + destruct (n0 ?= p0) eqn:NP0; try (inversion EQ1; fail). eapply Pos.compare_eq in NP0. subst. inv EQ1. + destruct (condition_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption. (* Ireturn *) - destruct i'; try (inversion H; fail). destruct (option_eq _ _ _); try discriminate. subst. clear H. |