aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-02 09:14:10 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-02 09:14:10 +0100
commit8aae10b50b321cfcbde86582cdd7ce1df8960628 (patch)
tree4e76f4d98f1bf97783c1f55fc5adcba415abfc41 /ia32
parent803eb70bbbbc5749882efd2a3af339a7e05f1f62 (diff)
downloadcompcert-8aae10b50b321cfcbde86582cdd7ce1df8960628.tar.gz
compcert-8aae10b50b321cfcbde86582cdd7ce1df8960628.zip
Starting to remove the seperate printers for each backend.
Diffstat (limited to 'ia32')
-rw-r--r--ia32/PrintAsm.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index b0ef0180..c77347da 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -98,6 +98,8 @@ module Cygwin_System =
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\", \"%s\"\n"
s (if ex then "xr" else if wr then "d" else "dr")
+ | Section_debug -> ".section .debug_info,\"\""
+ | Section_debug_abbrev -> ".section .debug_abbrev,\"\""
let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
@@ -147,7 +149,10 @@ module ELF_System =
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\",\"a%s%s\",@progbits"
s (if wr then "w" else "") (if ex then "x" else "")
+ | Section_debug -> sprintf ".section .debug_info,\"\",@progbits"
+ | Section_debug_abbrev -> sprintf ".section .debug_abbrev,\"\",@progbits"
+
let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
let print_align oc n =
@@ -201,6 +206,8 @@ module MacOS_System =
sprintf ".section \"%s\", %s, %s"
(if wr then "__DATA" else "__TEXT") s
(if ex then "regular, pure_instructions" else "regular")
+ | Section_debug -> ".section __DWARF,__debug_info,regular,debug"
+ | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug"
let stack_alignment = 16 (* mandatory *)