From c9acadca7c8d5d29dd57b9acba99369067f93ae1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 8 Sep 2010 16:50:23 +0000
Subject: 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
---
 ia32/PrintAsm.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'ia32')

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 32bb073b..f3cb519e 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
 
-- 
cgit