diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-22 16:18:22 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-22 16:18:22 +0100 |
commit | 6acefcbbc51aa7d2edb7b2098a5b15d06e742604 (patch) | |
tree | 7c82b4e1c690ec27171dab9c15630818f08270c9 /mppa_k1c/Asmblockgenproof1.v | |
parent | 8909fb3df6fd282d6b8f24b288ef5d7ddbdb741a (diff) | |
download | compcert-kvx-6acefcbbc51aa7d2edb7b2098a5b15d06e742604.tar.gz compcert-kvx-6acefcbbc51aa7d2edb7b2098a5b15d06e742604.zip |
Added sxwd and zxwd support
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 2b653236..02301161 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1068,7 +1068,7 @@ Qed. (** Some arithmetic properties. *) -Remark cast32unsigned_from_cast32signed: +(* Remark cast32unsigned_from_cast32signed: forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). Proof. intros. apply Int64.same_bits_eq; intros. @@ -1096,7 +1096,7 @@ Proof. + split. * Simpl. * intros. destruct r; Simpl. -Qed. +Qed. *) (* Translation of arithmetic operations *) @@ -1169,12 +1169,12 @@ Opaque Int.eq. eapply exec_straight_step. simpl; reflexivity. auto. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. -- (* Ocast32signed *) +(* - (* Ocast32signed *) exploit cast32signed_correct; eauto. intros (rs' & A & B & C). exists rs'; split; eauto. split. apply B. intros. assert (r <> PC). { destruct r; auto; contradict H; discriminate. } apply C; auto. -- (* longofintu *) + *)(* - (* longofintu *) econstructor; split. eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. split; intros; Simpl. (* unfold Pregmap.set; Simpl. *) destruct (PregEq.eq x0 x0). @@ -1182,7 +1182,7 @@ Opaque Int.eq. assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. - + contradict n. auto. + + contradict n. auto. *) - (* Ocmp *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. |