Commit a9578873 authored by xleroy's avatar xleroy
Browse files

Revised signed/unsigned char handling.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 1132f086
......@@ -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
......
......@@ -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)
......
......@@ -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
......
......@@ -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;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment