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/ValueAOp.v | |
| parent | b2e35bf85d1d1db02aa7f74ee45a47f79463d99f (diff) | |
| download | compcert-kvx-3750a2ad965b4959f6535aeeb9075dbd1a7c0527.tar.gz compcert-kvx-3750a2ad965b4959f6535aeeb9075dbd1a7c0527.zip | |
selectl generation
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index f181c0ea..a3843301 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -52,8 +52,8 @@ Definition select (v0 v1 vselect : aval) : aval := Definition selectl (v0 v1 vselect : aval) : aval := match vselect with - | I iselect => - if Int.eq Int.zero iselect + | L iselect => + if Int64.eq Int64.zero iselect then binop_long (fun x0 x1 => x0) v0 v1 else binop_long (fun x0 x1 => x1) v0 v1 | _ => Vtop @@ -272,12 +272,8 @@ Proof. destruct a1; destruct a0; eauto; constructor. (* selectl *) - inv H2; simpl; try constructor. - + destruct (Int.eq _ _); apply binop_long_sound; trivial. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); + + destruct (Int64.eq _ _); apply binop_long_sound; trivial. + + destruct (Int64.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. |