Treat "char" as unsigned OR signed depending on the configuration.

Fixed infinite expansion of some recursive struct type where recursion goes through a typeded.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1596 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 58 insertions, 10 deletions

diff --git a/Makefile b/Makefile
index 6fea519..c47ac40 100644
--- a/Makefile
+++ b/Makefile
@@ -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 b6ab3ba..284b825 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 ->
diff --git a/configure b/configure
index 5744c54..8f8c829 100755
--- a/configure
+++ b/configure
@@ -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 d6d1868..54a9c47 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 a385cc4..eda31de 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 0000000..708031e
--- /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 0000000..9da4f52
--- /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 0000000..7ae6bb0
--- /dev/null
+++ b/test/regression/struct10.c
@@ -0,0 +1,5 @@
+typedef struct xs X;
+
+struct xs {
+  X *x; 
+} x0;