diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-08 16:50:23 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-08 16:50:23 +0000 |
commit | c9acadca7c8d5d29dd57b9acba99369067f93ae1 (patch) | |
tree | 9041580ba55ec85af830d61c0b566b0432df0319 /ia32/PrintAsm.ml | |
parent | 28c04de64220be15c589c4dbe1662b212b6d25b1 (diff) | |
download | compcert-c9acadca7c8d5d29dd57b9acba99369067f93ae1.tar.gz compcert-c9acadca7c8d5d29dd57b9acba99369067f93ae1.zip |
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
Diffstat (limited to 'ia32/PrintAsm.ml')
-rw-r--r-- | ia32/PrintAsm.ml | 18 |
1 files changed, 9 insertions, 9 deletions
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 |