diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 10:04:26 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 10:04:26 +0100 |
| commit | 0921a0b5bafb179f18f94561bece26a4d184fa31 (patch) | |
| tree | 602eb4b7962800d71483f4c689f77c26f40edb9c /ia32 | |
| parent | fe57280950fc20b2d1650a022033484b152ae51d (diff) | |
| download | compcert-0921a0b5bafb179f18f94561bece26a4d184fa31.tar.gz compcert-0921a0b5bafb179f18f94561bece26a4d184fa31.zip | |
Changed the symbol function back to its old definition.
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/PrintAsm.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index b0ef0180..d064782e 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -60,7 +60,6 @@ let preg oc = function module type SYSTEM = sig val raw_symbol: out_channel -> string -> unit - val symbol: out_channel -> P.t -> unit val label: out_channel -> int -> unit val name_of_section: section_name -> string val stack_alignment: int @@ -80,9 +79,6 @@ module Cygwin_System = let raw_symbol oc s = fprintf oc "_%s" s - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) - let label oc lbl = fprintf oc "L%d" lbl @@ -128,9 +124,6 @@ module ELF_System = let raw_symbol oc s = fprintf oc "%s" s - - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) let label oc lbl = fprintf oc ".L%d" lbl @@ -182,9 +175,6 @@ module MacOS_System = let raw_symbol oc s = fprintf oc "_%s" s - let symbol oc symb = - fprintf oc "_%s" (extern_atom symb) - let label oc lbl = fprintf oc "L%d" lbl @@ -249,6 +239,9 @@ module AsmPrinter(Target: SYSTEM) = open Target (* On-the-fly label renaming *) +let symbol oc symb = + raw_symbol oc (extern_atom symb) + let next_label = ref 100 let new_label() = |