aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionaux.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-06-04 11:47:14 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-06-04 11:47:14 +0200
commit5feecb99712de3604f284e5934aed73f2b606659 (patch)
treedfe87bad1fe089f83d82a452d1d8886d2dc17ab1 /backend/Selectionaux.ml
parenteec7948bd0204787ad8ddde70c5a28fdfd62356a (diff)
downloadcompcert-kvx-5feecb99712de3604f284e5934aed73f2b606659.tar.gz
compcert-kvx-5feecb99712de3604f284e5934aed73f2b606659.zip
start to have whole path if-conversion?
Diffstat (limited to 'backend/Selectionaux.ml')
-rw-r--r--backend/Selectionaux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index b43b0e7f..b25f1fa1 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -76,7 +76,7 @@ let fast_cmove ty =
| "riscV", _ -> false
| "x86", _ ->
(match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
- | "mppa_k1c", _ -> false (* TODO DM *)
+ | "mppa_k1c", _ -> true
| a, m -> failwith (Printf.sprintf "fast_cmove: unknown arch %s %s" a m)
(* The if-conversion heuristic depend on the