diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 06:07:00 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 06:07:00 +0200 |
| commit | 70db0c8a5cd5fb21e92de32cc4eb5774baf60610 (patch) | |
| tree | f536411ac4750bc186b6d2f6a7afdfaaa345d729 /mppa_k1c/Asmblockgenproof1.v | |
| parent | ca34ea47f863c074a9d0ca890097786c5829267c (diff) | |
| download | compcert-kvx-70db0c8a5cd5fb21e92de32cc4eb5774baf60610.tar.gz compcert-kvx-70db0c8a5cd5fb21e92de32cc4eb5774baf60610.zip | |
prepare for conditions in cmove
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index f75f0bd3..698d64d6 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1642,7 +1642,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold select. + * unfold eval_select. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1656,7 +1656,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectl. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1670,7 +1670,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectf. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1684,7 +1684,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectfs. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. |