diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 22:44:31 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 22:44:31 +0100 |
| commit | 3750a2ad965b4959f6535aeeb9075dbd1a7c0527 (patch) | |
| tree | 49a8dc8909c57fa71cab64ca0041fed968d57776 /mppa_k1c/Asmblockgenproof1.v | |
| parent | b2e35bf85d1d1db02aa7f74ee45a47f79463d99f (diff) | |
| download | compcert-kvx-3750a2ad965b4959f6535aeeb9075dbd1a7c0527.tar.gz compcert-kvx-3750a2ad965b4959f6535aeeb9075dbd1a7c0527.zip | |
selectl generation
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index a1bd7124..16663522 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1568,6 +1568,16 @@ Proof. destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. Qed. +Lemma int64_eq_comm: + forall (x y: int64), + (Int64.eq x y) = (Int64.eq y x). +Proof. + intros. + unfold Int64.eq. + unfold zeq. + destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. +Qed. + Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> @@ -1674,13 +1684,13 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold select. + * unfold selectl. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. simpl. - rewrite int_eq_comm. - destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + rewrite int64_eq_comm. + destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. |