diff options
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 3 | ||||
-rwxr-xr-x | configure | 14 | ||||
-rw-r--r-- | driver/Driver.ml | 8 |
4 files changed, 8 insertions, 18 deletions
@@ -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 284b825b..23d05029 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) @@ -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 54a9c47e..ee48ffca 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; |