diff options
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 16 | ||||
-rwxr-xr-x | configure | 14 | ||||
-rw-r--r-- | driver/Driver.ml | 4 | ||||
-rw-r--r-- | test/regression/Makefile | 4 | ||||
-rw-r--r-- | test/regression/Results/char1 | 8 | ||||
-rw-r--r-- | test/regression/char1.c | 16 | ||||
-rw-r--r-- | test/regression/struct10.c | 5 |
8 files changed, 58 insertions, 10 deletions
@@ -151,6 +151,7 @@ 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 b6ab3ba3..284b825b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -239,7 +239,7 @@ let convertInt n = coqint_of_camlint(Int64.to_int32 n) let convertIkind = function | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8) - | C.IChar -> (Unsigned, I8) + | C.IChar -> ((if Configuration.signed_char then Signed else Unsigned), I8) | C.ISChar -> (Signed, I8) | C.IUChar -> (Unsigned, I8) | C.IInt -> (Signed, I32) @@ -275,12 +275,15 @@ let convertTyp env t = let (sg, sz) = convertIkind ik in Tint(sz, sg) | C.TFloat(fk, a) -> Tfloat(convertFkind fk) - | C.TPtr(C.TStruct(id, _), _) when List.mem id seen -> - Tcomp_ptr(intern_string ("struct " ^ id.name)) - | C.TPtr(C.TUnion(id, _), _) when List.mem id seen -> - Tcomp_ptr(intern_string ("union " ^ id.name)) | C.TPtr(ty, a) -> - Tpointer(convertTyp seen ty) + begin match Cutil.unroll env ty with + | C.TStruct(id, _) when List.mem id seen -> + Tcomp_ptr(intern_string ("struct " ^ id.name)) + | C.TUnion(id, _) when List.mem id seen -> + Tcomp_ptr(intern_string ("union " ^ id.name)) + | _ -> + Tpointer(convertTyp seen ty) + end | C.TArray(ty, None, a) -> (* Cparser verified that the type ty[] occurs only in contexts that are safe for Clight, so just treat as ty[0]. *) @@ -810,7 +813,6 @@ let convertInit env ty init = | Some(C.CEnum _) -> error "enum tag after constant folding" | None -> - Format.printf "%a@." Cprint.exp (0, e); error "initializer is not a compile-time constant" end | Init_array il -> @@ -70,6 +70,7 @@ 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" @@ -80,6 +81,7 @@ case "$target" in arch="powerpc" variant="eabi" system="linux" + signed_char="false" cc="gcc" cprepro="gcc -U__GNUC__ -E" casm="gcc -c" @@ -90,6 +92,7 @@ case "$target" in arch="arm" variant="linux" system="linux" + signed_char="false" cc="gcc" cprepro="gcc -U__GNUC__ -E" casm="gcc -c" @@ -100,6 +103,7 @@ 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" @@ -110,6 +114,7 @@ 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" @@ -120,6 +125,7 @@ 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" @@ -130,6 +136,7 @@ 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" @@ -162,6 +169,7 @@ cat >> Makefile.config <<EOF ARCH=$arch VARIANT=$variant SYSTEM=$system +SIGNED_CHAR=$signed_char CC=$cc CPREPRO=$cprepro CASM=$casm @@ -199,6 +207,11 @@ 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 @@ -242,6 +255,7 @@ 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 d6d18689..54a9c47e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -357,7 +357,9 @@ let cmdline_actions = let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; - Cparser.Machine.config := Cparser.Machine.ilp32ll64; + Cparser.Machine.config := + { Cparser.Machine.ilp32ll64 + with Cparser.Machine.char_signed = Configuration.signed_char }; Cparser.Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions usage_string; diff --git a/test/regression/Makefile b/test/regression/Makefile index a385cc48..eda31dee 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -11,12 +11,12 @@ LIBS=$(LIBMATH) TESTS=bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 \ expr1 initializers volatile2 \ - funct3 expr5 struct7 struct8 casts1 casts2 + funct3 expr5 struct7 struct8 casts1 casts2 char1 # Other tests: should compile to .s without errors (but expect warnings) EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \ init2 init3 init4 pragmas ptrs1 ptrs2 sizeof1 struct1 struct2 struct3 \ - struct4 struct5 struct6 struct9 types1 volatile1 + struct4 struct5 struct6 struct9 struct10 types1 volatile1 # Test known to fail FAILURES=funct1 varargs1 diff --git a/test/regression/Results/char1 b/test/regression/Results/char1 new file mode 100644 index 00000000..708031ef --- /dev/null +++ b/test/regression/Results/char1 @@ -0,0 +1,8 @@ +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 diff --git a/test/regression/char1.c b/test/regression/char1.c new file mode 100644 index 00000000..9da4f52e --- /dev/null +++ b/test/regression/char1.c @@ -0,0 +1,16 @@ +#include <stdio.h> +#include <limits.h> + +int foo (char x) { + char y = x; + return ++x > y; +} + +int main (void) { + int i; + for (i=CHAR_MIN; i<=CHAR_MAX; i++) { + printf ("%d ", foo(i)); + if ((i&31)==31) printf ("\n"); + } + return 0; +} diff --git a/test/regression/struct10.c b/test/regression/struct10.c new file mode 100644 index 00000000..7ae6bb0d --- /dev/null +++ b/test/regression/struct10.c @@ -0,0 +1,5 @@ +typedef struct xs X; + +struct xs { + X *x; +} x0; |