diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-05 14:25:21 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-05 14:25:21 +0200 |
| commit | 5a095e968ca040757db22a4bd7cde34b91bf44e1 (patch) | |
| tree | a3c934884d3a4c55f90e76962ea39d74013b9b9c /mppa_k1c/Asmvliw.v | |
| parent | 2e1ecb87d05d7a6b5921be04ba10f6b9eae1be9c (diff) | |
| download | compcert-kvx-5a095e968ca040757db22a4bd7cde34b91bf44e1.tar.gz compcert-kvx-5a095e968ca040757db22a4bd7cde34b91bf44e1.zip | |
Removing unused .all, .any, .nall and .none conditions
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 54654abb..54e9c847 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -203,11 +203,6 @@ Inductive itest: Type := | ITgeu (**r Greater Than or Equal Unsigned *) | ITleu (**r Less Than or Equal Unsigned *) | ITgtu (**r Greater Than Unsigned *) - (* Not used yet *) - | ITall (**r All Bits Set in Mask *) - | ITnall (**r Not All Bits Set in Mask *) - | ITany (**r Any Bits Set in Mask *) - | ITnone (**r Not Any Bits Set in Mask *) . Inductive ftest: Type := @@ -909,10 +904,6 @@ Definition compare_int (t: itest) (v1 v2: val): val := | ITgeu => Val_cmpu Cge v1 v2 | ITleu => Val_cmpu Cle v1 v2 | ITgtu => Val_cmpu Cgt v1 v2 - | ITall - | ITnall - | ITany - | ITnone => Vundef end. Definition compare_long (t: itest) (v1 v2: val): val := @@ -929,10 +920,6 @@ Definition compare_long (t: itest) (v1 v2: val): val := | ITgeu => Some (Val_cmplu Cge v1 v2) | ITleu => Some (Val_cmplu Cle v1 v2) | ITgtu => Some (Val_cmplu Cgt v1 v2) - | ITall - | ITnall - | ITany - | ITnone => Some Vundef end in match res with | Some v => v |