diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 21:16:40 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 21:16:40 +0200 |
| commit | ac366a59308ae85a0cbfefb8b9be79763d5c5f91 (patch) | |
| tree | b533ea1790cf2b169c98e6af707b7e98b39869ac /mppa_k1c/Asmblockgenproof1.v | |
| parent | ed95a6a6fbdd915e361e696d4bf72e5a545b965e (diff) | |
| download | compcert-kvx-ac366a59308ae85a0cbfefb8b9be79763d5c5f91.tar.gz compcert-kvx-ac366a59308ae85a0cbfefb8b9be79763d5c5f91.zip | |
added immediate cmove
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 1ed584e8..8939cc30 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1759,9 +1759,11 @@ Opaque Int.eq. destruct (Int.ltu _ _); simpl; trivial. * intros. rewrite Pregmap.gso; trivial. + - (* Ocmp *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. + - (* Osel *) unfold conditional_move in *. destruct (ireg_eq _ _). @@ -1784,6 +1786,7 @@ Opaque Int.eq. econstructor; split; try (apply exec_straight_one; constructor); split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption); unfold Val.select; simpl; + unfold cmove, cmoveu; rewrite Pregmap.gss; destruct (rs x1); simpl; trivial; try rewrite int_ltu_to_neq; |