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/Op.v | |
| parent | b2e35bf85d1d1db02aa7f74ee45a47f79463d99f (diff) | |
| download | compcert-kvx-3750a2ad965b4959f6535aeeb9075dbd1a7c0527.tar.gz compcert-kvx-3750a2ad965b4959f6535aeeb9075dbd1a7c0527.zip | |
selectl generation
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 39a599d8..ec3f1077 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -271,12 +271,12 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : val := Definition selectl (v0 : val) (v1 : val) (vselect : val) : val := match vselect with - | Vint iselect => + | Vlong iselect => match v0 with | Vlong i0 => match v1 with | Vlong i1 => - Vlong (if Int.cmp Ceq Int.zero iselect + Vlong (if Int64.cmp Ceq Int64.zero iselect then i0 else i1) | _ => Vundef |