summaryrefslogtreecommitdiff
path: root/driver
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-03-10 10:12:09 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-03-10 10:12:09 +0000
commita9578873a5bdf14c47650cc3dd9d21e3bcef2370 (patch)
treefb536f66c392c2d82ab5f5ac45b53ea12ac20b63 /driver
parent1132f0865a3d5fe3dd43b1d2d9c4580e10436107 (diff)
Revised signed/unsigned char handling.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r--driver/Driver.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 54a9c47..ee48ffc 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -358,8 +358,12 @@ let cmdline_actions =
let _ =
Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };
Cparser.Machine.config :=
- { Cparser.Machine.ilp32ll64
- with Cparser.Machine.char_signed = Configuration.signed_char };
+ begin match Configuration.arch with
+ | "powerpc" -> Cparser.Machine.ppc_32_bigendian
+ | "arm" -> Cparser.Machine.arm_littleendian
+ | "ia32" -> Cparser.Machine.x86_32
+ | _ -> assert false
+ end;
Cparser.Builtins.set C2C.builtins;
CPragmas.initialize();
parse_cmdline cmdline_actions usage_string;