aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-06-10 18:33:58 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-06-10 18:33:58 +0200
commita0ad5ff6f9c7603610a7448935b36c9ed22c6435 (patch)
tree2ec8247b4ea1e10c781a2d13ed30b7a483380956 /x86
parent9eccbd39710aab5d6bfe021c57f50a1916d37f70 (diff)
downloadcompcert-kvx-a0ad5ff6f9c7603610a7448935b36c9ed22c6435.tar.gz
compcert-kvx-a0ad5ff6f9c7603610a7448935b36c9ed22c6435.zip
x86 assembly: fix the comment delimiter for macos and make it per-OS
As reported in #399, it seems better to use `##` instead of `#` as comment delimiter under macOS. For the time being we keep using `#` for Linux and Cygwin. Closes: #399
Diffstat (limited to 'x86')
-rw-r--r--x86/TargetPrinter.ml14
1 files changed, 11 insertions, 3 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 1b27ee73..5bc2be1c 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n)
let data_pointer = if Archi.ptr64 then ".quad" else ".long"
-(* The comment deliminiter *)
-let comment = "#"
-
(* Base-2 log of a Caml integer *)
let rec log2 n =
assert (n > 0);
@@ -106,6 +103,7 @@ let rec log2 n =
(* System dependent printer functions *)
module type SYSTEM =
sig
+ val comment: string
val raw_symbol: out_channel -> string -> unit
val symbol: out_channel -> P.t -> unit
val label: out_channel -> int -> unit
@@ -124,6 +122,9 @@ module type SYSTEM =
module ELF_System : SYSTEM =
struct
+ (* The comment delimiter *)
+ let comment = "#"
+
let raw_symbol oc s =
fprintf oc "%s" s
@@ -180,6 +181,10 @@ module ELF_System : SYSTEM =
module MacOS_System : SYSTEM =
struct
+ (* The comment delimiter.
+ `##` instead of `#` to please the Clang assembler. *)
+ let comment = "##"
+
let raw_symbol oc s =
fprintf oc "_%s" s
@@ -239,6 +244,9 @@ module MacOS_System : SYSTEM =
module Cygwin_System : SYSTEM =
struct
+ (* The comment delimiter *)
+ let comment = "#"
+
let symbol_prefix =
if Archi.ptr64 then "" else "_"