diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-08-20 10:22:35 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-08-20 10:22:35 +0200 |
commit | 6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431 (patch) | |
tree | 27fd2d801607ee940e5254869c775f3662b4088b /driver/Frontend.ml | |
parent | ec8d93afc8875dcf7dfeb982eab255f150a91074 (diff) | |
download | compcert-6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431.tar.gz compcert-6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431.zip |
Add sizeof_reg and new Machine configurations (#129)
Since the size of integer registers is not identical to the size of pointers
for the ppc64 and e5500 model the check for register pairs in
ExtendedAsm does not work correctly.
In order to avoid this a new field sizeof_intreg is introduced in the
Machine configuration which describes the size of integer registers.
New configurations for the ppc64 and e5500 model are added
and used.
Bug 24273
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r-- | driver/Frontend.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml index e5b51c1f..88b47854 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -73,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 |