summaryrefslogtreecommitdiff
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
parent1132f0865a3d5fe3dd43b1d2d9c4580e10436107 (diff)
Revised signed/unsigned char handling.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--Makefile1
-rw-r--r--cfrontend/C2C.ml3
-rwxr-xr-xconfigure14
-rw-r--r--driver/Driver.ml8
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;