aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionaux.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-05-26 22:04:20 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-05-26 22:04:20 +0200
commitb4a08d0815342b6238d307864f0823d0f07bb691 (patch)
tree85f48254ca79a6e2bc9d7359017a5731f98f897f /backend/Selectionaux.ml
parent490a6caea1a95cfdbddf7aca244fa6a1c83aa9a2 (diff)
downloadcompcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.tar.gz
compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.zip
k1c -> kvx changes
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 5a8bde8c..fcf8e238 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -79,7 +79,7 @@ let fast_cmove ty =
| "riscV", _ -> false
| "x86", _ ->
(match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
- | "mppa_k1c", _ -> true
+ | "kvx", _ -> true
| a, m -> failwith (Printf.sprintf "fast_cmove: unknown arch %s %s" a m)
(* The if-conversion heuristic depend on the