aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-10-01 17:25:18 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-10-01 17:25:18 +0200
commite637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (patch)
tree518d558674d3e1c6ff41c46d84c784e727ed5d04 /driver/Driver.ml
parentad2a2c862abef3aee701d1bca0524fcbf2d07b30 (diff)
downloadcompcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.tar.gz
compcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.zip
Support for 64-bit architectures: generic support
- Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b89d93c1..4bd08a88 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -536,9 +536,12 @@ let _ =
| "arm" -> if Configuration.is_big_endian
then Machine.arm_bigendian
else Machine.arm_littleendian
- | "ia32" -> if Configuration.abi = "macosx"
- then Machine.x86_32_macosx
- else Machine.x86_32
+ | "ia32" -> if Configuration.model = "64" then
+ Machine.x86_64
+ else
+ if Configuration.abi = "macosx"
+ then Machine.x86_32_macosx
+ else Machine.x86_32
| _ -> assert false
end;
Builtins.set C2C.builtins;