aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 6133291e..ecf3d6a5 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -116,6 +116,11 @@ let init () =
| "riscV" -> if Configuration.model = "64"
then Machine.rv64
else Machine.rv32
+ | "kvx" -> if Configuration.os = "cos" then Machine.kvxcos
+ else if Configuration.os = "mbr" then Machine.kvxmbr
+ else if Configuration.os = "elf" then Machine.kvxelf
+ else (Printf.eprintf "Configuration OS = %s\n" Configuration.os;
+ failwith "Wrong OS configuration for KVX")
| "aarch64" -> if Configuration.abi = "apple"
then Machine.aarch64_apple
else Machine.aarch64