diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 11:16:42 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 11:16:42 +0100 |
| commit | b873e06abcee1c7f6a51aaabb973b550a52a5b61 (patch) | |
| tree | 70ccd9c7cbba08e20b782217b1a2268b1afce3e9 /driver/Frontend.ml | |
| parent | 65db9a4a02c30d8dd5ca89b6fe3e4524cd4c29a5 (diff) | |
| parent | eb7bd26e2b9eeed21d204bad26fa56c8a7937ffb (diff) | |
| download | compcert-kvx-b873e06abcee1c7f6a51aaabb973b550a52a5b61.tar.gz compcert-kvx-b873e06abcee1c7f6a51aaabb973b550a52a5b61.zip | |
Merge tag 'v3.4' into mppa_k1c
Conflicts:
.gitignore
Diffstat (limited to 'driver/Frontend.ml')
| -rw-r--r-- | driver/Frontend.ml | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml index db84a9f9..b29bb7f3 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -17,6 +17,15 @@ open Driveraux (* Common frontend functions between clightgen and ccomp *) +let predefined_macros = + [ + "-D__COMPCERT__"; + "-U__STDC_IEC_559_COMPLEX__"; + "-D__STDC_NO_ATOMICS__"; + "-D__STDC_NO_COMPLEX__"; + "-D__STDC_NO_THREADS__"; + "-D__STDC_NO_VLA__" + ] (* From C to preprocessed C *) @@ -26,7 +35,7 @@ let preprocess ifile ofile = if ofile = "-" then None else Some ofile in let cmd = List.concat [ Configuration.prepro; - ["-D__COMPCERT__"]; + predefined_macros; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] else []); @@ -64,10 +73,12 @@ let parse_c_file sourcename ifile = let init () = Machine.config:= begin match Configuration.arch with - | "powerpc" -> if Configuration.gnu_toolchain - then if Configuration.abi = "linux" - then Machine.ppc_32_linux_bigendian - else Machine.ppc_32_bigendian + | "powerpc" -> if Configuration.model = "e5500" || Configuration.model = "ppc64" + then if Configuration.abi = "linux" then Machine.ppc_32_r64_linux_bigendian + else if Configuration.gnu_toolchain then Machine.ppc_32_r64_bigendian + else Machine.ppc_32_r64_diab_bigendian + else if Configuration.abi = "linux" then Machine.ppc_32_linux_bigendian + else if Configuration.gnu_toolchain then Machine.ppc_32_bigendian else Machine.ppc_32_diab_bigendian | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian @@ -116,7 +127,7 @@ let gnu_prepro_actions = [ Exact "-imacros", String (gnu_prepro_opt_key "-imacros"); Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter"); Exact "-isystem", String (gnu_prepro_opt_key "-isystem"); - Exact "-iquote", String (gnu_prepro_opt_key "-iquore"); + Exact "-iquote", String (gnu_prepro_opt_key "-iquote"); Exact "-P", Self gnu_prepro_opt; Exact "-C", Self gnu_prepro_opt; Exact "-CC", Self gnu_prepro_opt;] |