aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
commitf16fa31ec9cc90da750c8cc10f447023962cd153 (patch)
tree28eed4d4b5bc964907f20332d1eed470a393d07b /driver/Frontend.ml
parent485a4c0dd450e65745c83e59acdb40b42058e556 (diff)
parentd703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff)
downloadcompcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.tar.gz
compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.zip
Merge branch 'kvx-work' into BTL
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index c8890046..480932df 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -109,8 +109,8 @@ let init () =
| "x86" -> if Configuration.model = "64" then
Machine.x86_64
else
- if Configuration.abi = "macosx"
- then Machine.x86_32_macosx
+ if Configuration.abi = "macos"
+ then Machine.x86_32_macos
else if Configuration.system = "bsd"
then Machine.x86_32_bsd
else Machine.x86_32
@@ -119,9 +119,12 @@ let init () =
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" -> Machine.aarch64
+ | "aarch64" -> if Configuration.abi = "apple"
+ then Machine.aarch64_apple
+ else Machine.aarch64
| _ -> assert false
end;
Env.set_builtins C2C.builtins;