diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-26 10:18:58 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-26 10:18:58 +0200 |
| commit | 0c00ace3c8981516ef02bc49f4e616e4cb485124 (patch) | |
| tree | f5600124386717114332368893aa521c36e7f0ca /backend/PrintAsmaux.ml | |
| parent | cc264a58d6fb43cf7c8ae41d73726dfedc20f1d4 (diff) | |
| download | compcert-kvx-0c00ace3c8981516ef02bc49f4e616e4cb485124.tar.gz compcert-kvx-0c00ace3c8981516ef02bc49f4e616e4cb485124.zip | |
Also quote \a.
This allows for an easier replacement of the binary address and
avoids that the user specifies his own binary addresses.
Bug 22468
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 07ab4bed..0db664ce 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -200,9 +200,11 @@ let annot_text preg_string sp_reg_name txt args = let ais_annot_list: (int * Str.split_result list) list ref = ref [] let re_annot_addr = Str.regexp "%addr" +let re_annot_quote = Str.regexp "\007" let ais_annot_text lbl preg_string sp_reg_name txt args = let annot = annot_text preg_string sp_reg_name txt args in + let annot = Str.global_replace re_annot_quote "\007\000" annot in let annots = Str.full_split re_annot_addr annot in ais_annot_list := (lbl,annots)::!ais_annot_list; annot |