Updates for IA32-Cygwin.

cparser/Elab.ml: tolerate changes in qualifiers in ?:
cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static.


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

5 files changed, 63 insertions, 33 deletions

diff --git a/Makefile b/Makefile
index 4237f2a..752a8e6 100644
--- a/Makefile
+++ b/Makefile
@@ -82,6 +82,14 @@ DRIVER=Compiler.v Complements.v
 
 FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER)
 
+# Symbolic links vs. copy
+
+ifneq (,$(findstring CYGWIN,$(shell uname -s)))
+SLN=cp
+else
+SLN=ln -s
+endif
+
 proof: $(FILES:.v=.vo)
 
 extraction:
@@ -91,15 +99,15 @@ extraction:
 
 ccomp: driver/Configuration.ml
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
-        && rm -f ccomp && ln -s _build/driver/Driver.native ccomp
+        && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp
 
 ccomp.prof: driver/Configuration.ml
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \
-        && rm -f ccomp.prof && ln -s _build/driver/Driver.p.native ccomp.prof
+        && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof
 
 ccomp.byte: driver/Configuration.ml
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
-        && rm -f ccomp.byte && ln -s _build/driver/Driver.d.byte ccomp.byte
+        && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte
 
 runtime:
 	$(MAKE) -C runtime
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 26815a1..b6ab3ba 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -25,7 +25,13 @@ open Csyntax
 (** Record the declarations of global variables and associate them
     with the corresponding atom. *)
 
-let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103
+type atom_info =
+  { a_storage: C.storage;
+    a_env: Env.t;
+    a_type: C.typ;
+    a_fundef: C.fundef option }
+
+let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103
 
 (** Hooks -- overriden in machine-dependent CPragmas module *)
 
@@ -135,10 +141,10 @@ let name_for_string_literal env s =
     let name = Printf.sprintf "__stringlit_%d" !stringNum in
     let id = intern_string name in
     Hashtbl.add decl_atom id
-      (env, (C.Storage_static,
-             Env.fresh_ident name,
-             C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
-             None));
+      { a_storage = C.Storage_static;
+        a_env = env;
+        a_type = C.TPtr(C.TInt(C.IChar,[C.AConst]),[]);
+        a_fundef = None };
     Sections.define_stringlit id;
     Hashtbl.add stringTable s id;
     id
@@ -701,9 +707,11 @@ let convertFundef env fd =
       fd.fd_locals in
   let body' = convertStmt env fd.fd_body in
   let id' = intern_string fd.fd_name.name in
-  let decl =
-    (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in
-  Hashtbl.add decl_atom id' (env, decl);
+  Hashtbl.add decl_atom id'
+    { a_storage = fd.fd_storage;
+      a_env = env;
+      a_type = Cutil.fundef_typ fd;
+      a_fundef = Some fd };
   Sections.define_function id';
   Datatypes.Coq_pair(id',
                      Internal {fn_return = ret; fn_params = params;
@@ -850,7 +858,7 @@ let rec type_is_volatile env t =
   | C.TArray(t', _, _) -> type_is_volatile env t'
   | _ -> false
 
-let convertGlobvar env (sto, id, ty, optinit as decl) =
+let convertGlobvar env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let ty' = convertTyp env ty in 
   let init' =
@@ -859,7 +867,11 @@ let convertGlobvar env (sto, id, ty, optinit as decl) =
         if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')]
     | Some i ->
         convertInit env ty i in
-  Hashtbl.add decl_atom id' (env, decl);
+  Hashtbl.add decl_atom id'
+    { a_storage = sto;
+      a_env = env;
+      a_type = ty;
+      a_fundef = None };
   Sections.define_variable id'
     (match Cutil.sizeof env ty with Some sz -> sz | None -> max_int)
     (type_is_readonly env ty);
@@ -978,36 +990,35 @@ let convertProgram p =
 
 let atom_is_static a =
   try
-    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
-    sto = C.Storage_static
+    match Hashtbl.find decl_atom a with
+    | { a_storage = C.Storage_static } -> true
+    (* We do not inline functions, but at least let's not make them globals *)
+    | { a_fundef = Some { fd_inline = true } } -> true 
+    | _ -> false
   with Not_found ->
     false
 
 let atom_is_extern a =
   try
-    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
-    sto = C.Storage_extern
+    let i = Hashtbl.find decl_atom a in i.a_storage = C.Storage_extern
   with Not_found ->
     false
 
 let atom_is_readonly a =
   try
-    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
-    type_is_readonly env ty
+    let i = Hashtbl.find decl_atom a in type_is_readonly i.a_env i.a_type
   with Not_found ->
     false
 
 let atom_sizeof a =
   try
-    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
-    Cutil.sizeof env ty
+    let i = Hashtbl.find decl_atom a in Cutil.sizeof i.a_env i.a_type
   with Not_found ->
     None
 
 let atom_alignof a =
   try
-    let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
-    Cutil.alignof env ty
+    let i = Hashtbl.find decl_atom a in Cutil.alignof i.a_env i.a_type
   with Not_found ->
     None
 
diff --git a/configure b/configure
index d49428d..5744c54 100755
--- a/configure
+++ b/configure
@@ -36,6 +36,7 @@ Supported targets:
   ia32-linux       (x86 32 bits, Linux)
   ia32-bsd         (x86 32 bits, BSD)
   ia32-macosx      (x86 32 bits, MacOS X)
+  ia32-cygwin      (x86 32 bits, Cygwin environment under Windows)
   manual           (edit configuration file by hand)
 
 Options:
@@ -125,6 +126,16 @@ case "$target" in
     clinker="gcc -arch i386"
     libmath=""
     need_stdlib_wrapper="true";;
+  ia32-cygwin)
+    arch="ia32"
+    variant="standard"
+    system="cygwin"
+    cc="gcc -m32"
+    cprepro="gcc -m32 -U__GNUC__ -E"
+    casm="gcc -m32 -c"
+    clinker="gcc -m32"
+    libmath="-lm"
+    need_stdlib_wrapper="false";;
   manual)
     ;;
   "")
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 2ae7c7e..b79aa10 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1021,7 +1021,7 @@ let elab_expr loc env a =
       | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) }
       | ty1, ty2 ->
-          match combine_types env ty1 ty2 with
+          match combine_types ~noattrs:true env ty1 ty2 with
           | None ->
               error ("the second and third arguments of '? :' have incompatible types")
           | Some tyres ->
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 32bb073..f3cb519 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -20,14 +20,14 @@ open Asm
 
 (* Recognition of target ABI and asm syntax *)
 
-type target = ELF | AOUT | MacOS
+type target = ELF | MacOS | Cygwin
 
 let target = 
   match Configuration.system with
   | "macosx" -> MacOS
   | "linux"  -> ELF
   | "bsd"    -> ELF
-  | "cygwin" -> AOUT
+  | "cygwin" -> Cygwin
   | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported")
 
 (* On-the-fly label renaming *)
@@ -55,7 +55,7 @@ let coqint oc n =
 let raw_symbol oc s =
   match target with
   | ELF -> fprintf oc "%s" s
-  | MacOS | AOUT -> fprintf oc "_%s" s
+  | MacOS | Cygwin -> fprintf oc "_%s" s
 
 let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$"
 
@@ -72,7 +72,7 @@ let symbol_offset oc (symb, ofs) =
 let label oc lbl =
   match target with
   | ELF -> fprintf oc ".L%d" lbl
-  | MacOS | AOUT -> fprintf oc "L%d" lbl
+  | MacOS | Cygwin -> fprintf oc "L%d" lbl
 
 let comment = "#"
 
@@ -146,7 +146,7 @@ let (text, data, const_data, float_literal, jumptable_literal) =
        ".const",
        ".const_data",
        ".text")
-  | AOUT ->
+  | Cygwin ->
       (".text",
        ".data",
        ".section	.rdata,\"dr\"",
@@ -157,8 +157,8 @@ let (text, data, const_data, float_literal, jumptable_literal) =
 
 let stack_alignment =
   match target with
-  | ELF | AOUT -> 8               (* minimum is 4, 8 is better for perfs *)
-  | MacOS -> 16                   (* mandatory *)
+  | ELF | Cygwin -> 8               (* minimum is 4, 8 is better for perfs *)
+  | MacOS -> 16                     (* mandatory *)
 
 let int32_align n a =
   if n >= 0l
@@ -184,8 +184,8 @@ let rec log2 n =
 
 let print_align oc n =
   match target with
-  | ELF          -> fprintf oc "	.align	%d\n" n
-  | AOUT | MacOS -> fprintf oc "	.align	%d\n" (log2 n)
+  | ELF | Cygwin -> fprintf oc "	.align	%d\n" n
+  | MacOS        -> fprintf oc "	.align	%d\n" (log2 n)
 
 let need_masks = ref false