aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
commita1c401a4eba5fc9fcf42933f70005ecb679a4c1c (patch)
tree26637fca5d1da9b3d049234721d593a60b03a6d3 /driver/Frontend.ml
parentc49caca4b5f0239b43610fbfe012d6ba0211b364 (diff)
parent1daf96cdca4d828c333cea5c9a314ef861342984 (diff)
downloadcompcert-dev/michalis.tar.gz
compcert-dev/michalis.zip
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index bb97e945..6133291e 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -80,7 +80,6 @@ let parse_c_file sourcename ifile =
let simplifs =
"b" (* blocks: mandatory *)
^ (if !option_fstruct_passing then "s" else "")
- ^ (if !option_fbitfields then "f" else "")
^ (if !option_fpacked_structs then "p" else "")
in
(* Parsing and production of a simplified C AST *)
@@ -109,15 +108,17 @@ 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
| "riscV" -> if Configuration.model = "64"
then Machine.rv64
else Machine.rv32
- | "aarch64" -> Machine.aarch64
+ | "aarch64" -> if Configuration.abi = "apple"
+ then Machine.aarch64_apple
+ else Machine.aarch64
| _ -> assert false
end;
Env.set_builtins C2C.builtins;