From a9578873a5bdf14c47650cc3dd9d21e3bcef2370 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 10 Mar 2011 10:12:09 +0000
Subject: Revised signed/unsigned char handling.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile         |  1 -
 cfrontend/C2C.ml |  3 ++-
 configure        | 14 --------------
 driver/Driver.ml |  8 ++++++--
 4 files changed, 8 insertions(+), 18 deletions(-)

diff --git a/Makefile b/Makefile
index ad01271..af61fcb 100644
--- a/Makefile
+++ b/Makefile
@@ -150,7 +150,6 @@ driver/Configuration.ml: Makefile.config
          echo 'let arch = "$(ARCH)"'; \
          echo 'let variant = "$(VARIANT)"'; \
          echo 'let system = "$(SYSTEM)"'; \
-         echo 'let signed_char = $(SIGNED_CHAR)'; \
          echo 'let need_stdlib_wrapper = $(NEED_STDLIB_WRAPPER)') \
         > driver/Configuration.ml
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 284b825..23d0502 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -239,7 +239,8 @@ let convertInt n = coqint_of_camlint(Int64.to_int32 n)
 
 let convertIkind = function
   | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8)
-  | C.IChar -> ((if Configuration.signed_char then Signed else Unsigned), I8)
+  | C.IChar -> ((if (!Cparser.Machine.config).Cparser.Machine.char_signed
+                 then Signed else Unsigned), I8)
   | C.ISChar -> (Signed, I8)
   | C.IUChar -> (Unsigned, I8)
   | C.IInt -> (Signed, I32)
diff --git a/configure b/configure
index 8f8c829..5744c54 100755
--- a/configure
+++ b/configure
@@ -70,7 +70,6 @@ case "$target" in
     arch="powerpc"
     variant="macosx"
     system="macosx"
-    signed_char="false"
     cc="gcc -arch ppc"
     cprepro="gcc -arch ppc -U__GNUC__ -U__BLOCKS__ -E"
     casm="gcc -arch ppc -c"
@@ -81,7 +80,6 @@ case "$target" in
     arch="powerpc"
     variant="eabi"
     system="linux"
-    signed_char="false"
     cc="gcc"
     cprepro="gcc -U__GNUC__ -E"
     casm="gcc -c"
@@ -92,7 +90,6 @@ case "$target" in
     arch="arm"
     variant="linux"
     system="linux"
-    signed_char="false"
     cc="gcc"
     cprepro="gcc -U__GNUC__ -E"
     casm="gcc -c"
@@ -103,7 +100,6 @@ case "$target" in
     arch="ia32"
     variant="standard"
     system="linux"
-    signed_char="true"
     cc="gcc -m32"
     cprepro="gcc -m32 -U__GNUC__ -E"
     casm="gcc -m32 -c"
@@ -114,7 +110,6 @@ case "$target" in
     arch="ia32"
     variant="standard"
     system="bsd"
-    signed_char="true"
     cc="gcc -m32"
     cprepro="gcc -m32 -U__GNUC__ -E"
     casm="gcc -m32 -c"
@@ -125,7 +120,6 @@ case "$target" in
     arch="ia32"
     variant="standard"
     system="macosx"
-    signed_char="true"
     cc="gcc -arch i386"
     cprepro="gcc -arch i386 -U__GNUC__ -U__BLOCKS__ -E"
     casm="gcc -arch i386 -c"
@@ -136,7 +130,6 @@ case "$target" in
     arch="ia32"
     variant="standard"
     system="cygwin"
-    signed_char="true"
     cc="gcc -m32"
     cprepro="gcc -m32 -U__GNUC__ -E"
     casm="gcc -m32 -c"
@@ -169,7 +162,6 @@ cat >> Makefile.config <<EOF
 ARCH=$arch
 VARIANT=$variant
 SYSTEM=$system
-SIGNED_CHAR=$signed_char
 CC=$cc
 CPREPRO=$cprepro
 CASM=$casm
@@ -207,11 +199,6 @@ VARIANT=
 # SYSTEM=cygwin
 SYSTEM=
 
-# Is the "char" type signed?
-#SIGNED_CHAR=false
-#SIGNED_CHAR=true
-SIGNED_CHAR=
-
 # C compiler for compiling library files
 CC=gcc
 
@@ -255,7 +242,6 @@ CompCert configuration:
     Target architecture........... $arch
     Application binary interface.. $variant
     OS and development env........ $system
-    "char" type is signed?........ $signed_char
     C compiler.................... $cc
     C preprocessor................ $cprepro
     Assembler..................... $casm
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;
-- 
cgit v1.2.3