diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 10:07:22 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 10:07:22 +0100 |
| commit | d4389977e95d3569ff0abb53e1b1fba20254b21e (patch) | |
| tree | f348e9a1c1f22cca2c168514ec2377d9ef1565d5 /ia32 | |
| parent | 0921a0b5bafb179f18f94561bece26a4d184fa31 (diff) | |
| download | compcert-d4389977e95d3569ff0abb53e1b1fba20254b21e.tar.gz compcert-d4389977e95d3569ff0abb53e1b1fba20254b21e.zip | |
Added back symbol functions in the different printer, since they are still needed.
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/PrintAsm.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index d064782e..036dbda8 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -60,6 +60,7 @@ 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 @@ -79,6 +80,9 @@ module Cygwin_System = let raw_symbol oc s = fprintf oc "_%s" s + let symbol oc s = + raw_symbol oc (extern_atom symb) + let label oc lbl = fprintf oc "L%d" lbl @@ -125,6 +129,9 @@ module ELF_System = let raw_symbol oc s = fprintf oc "%s" s + let symbol oc s = + raw_symbol oc (extern_atom symb) + let label oc lbl = fprintf oc ".L%d" lbl @@ -175,6 +182,9 @@ module MacOS_System = let raw_symbol oc s = fprintf oc "_%s" s + let symbol oc s = + raw_symbol oc (extern_atom symb) + let label oc lbl = fprintf oc "L%d" lbl @@ -239,9 +249,6 @@ 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() = |